Commit ac08b166 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

add scrollbar on left toolbox

parent 05e29627
...@@ -103,6 +103,8 @@ NON PRIORITAIRE ? ...@@ -103,6 +103,8 @@ NON PRIORITAIRE ?
* efficiency issues * efficiency issues
** understand problems when large number of goals (cf D Mentré examples) ** understand problems when large number of goals (cf D Mentré examples)
** also: BTS 13736
https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* ALL fix bug and update the BTS * ALL fix bug and update the BTS
** reject global "val"s in typing environment for logic decls. ** reject global "val"s in typing environment for logic decls.
......
...@@ -184,15 +184,23 @@ let factory = new GMenu.factory menubar ...@@ -184,15 +184,23 @@ let factory = new GMenu.factory menubar
let accel_group = factory#accel_group let accel_group = factory#accel_group
let hb = GPack.hbox ~packing:vbox#add ~border_width:2 () let hb = GPack.hbox ~packing:vbox#add ()
let left_scrollview =
try
GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC
~packing:(hb#pack ~expand:false) ()
with Gtk.Error _ -> assert false
let () = left_scrollview#set_shadow_type `OUT
let tools_window_vbox = let tools_window_vbox =
try try
GPack.vbox ~packing:(hb#pack ~expand:false) ~border_width:2 () GPack.vbox ~packing:left_scrollview#add_with_viewport ()
with Gtk.Error _ -> assert false with Gtk.Error _ -> assert false
let context_frame = let context_frame =
GBin.frame ~label:"Context" GBin.frame ~label:"Context" ~shadow_type:`ETCHED_OUT
~packing:(tools_window_vbox#pack ~expand:false) () ~packing:(tools_window_vbox#pack ~expand:false) ()
let context_box = let context_box =
...@@ -223,9 +231,10 @@ let () = ...@@ -223,9 +231,10 @@ let () =
let provers_frame = let provers_frame =
GBin.frame ~label:"Provers" GBin.frame ~label:"Provers" ~shadow_type:`ETCHED_OUT
~packing:(tools_window_vbox#pack ~expand:false) () ~packing:(tools_window_vbox#pack ~expand:false) ()
let provers_box = let provers_box =
GPack.button_box `VERTICAL ~border_width:5 ~spacing:5 GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
~packing:provers_frame#add () ~packing:provers_frame#add ()
...@@ -233,7 +242,7 @@ let provers_box = ...@@ -233,7 +242,7 @@ let provers_box =
let () = provers_frame#set_resize_mode `PARENT let () = provers_frame#set_resize_mode `PARENT
let transf_frame = let transf_frame =
GBin.frame ~label:"Transformations" GBin.frame ~label:"Transformations" ~shadow_type:`ETCHED_OUT
~packing:(tools_window_vbox#pack ~expand:false) () ~packing:(tools_window_vbox#pack ~expand:false) ()
let transf_box = let transf_box =
...@@ -241,7 +250,7 @@ let transf_box = ...@@ -241,7 +250,7 @@ let transf_box =
~packing:transf_frame#add () ~packing:transf_frame#add ()
let tools_frame = let tools_frame =
GBin.frame ~label:"Tools" GBin.frame ~label:"Tools" ~shadow_type:`ETCHED_OUT
~packing:(tools_window_vbox#pack ~expand:false) () ~packing:(tools_window_vbox#pack ~expand:false) ()
let tools_box = let tools_box =
...@@ -249,7 +258,7 @@ let tools_box = ...@@ -249,7 +258,7 @@ let tools_box =
~packing:tools_frame#add () ~packing:tools_frame#add ()
let cleaning_frame = let cleaning_frame =
GBin.frame ~label:"Cleaning" GBin.frame ~label:"Cleaning" ~shadow_type:`ETCHED_OUT
~packing:(tools_window_vbox#pack ~expand:false) () ~packing:(tools_window_vbox#pack ~expand:false) ()
let cleaning_box = let cleaning_box =
...@@ -257,7 +266,7 @@ let cleaning_box = ...@@ -257,7 +266,7 @@ let cleaning_box =
~packing:cleaning_frame#add () ~packing:cleaning_frame#add ()
let monitor_frame = let monitor_frame =
GBin.frame ~label:"Proof monitoring" GBin.frame ~label:"Proof monitoring" ~shadow_type:`ETCHED_OUT
~packing:(tools_window_vbox#pack ~expand:false) () ~packing:(tools_window_vbox#pack ~expand:false) ()
let monitor_box = let monitor_box =
...@@ -283,11 +292,10 @@ let hp = GPack.paned `HORIZONTAL ~packing:hb#add () ...@@ -283,11 +292,10 @@ let hp = GPack.paned `HORIZONTAL ~packing:hb#add ()
let scrollview = let scrollview =
try try
GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
~width:gconfig.tree_width ~width:gconfig.tree_width ~shadow_type:`ETCHED_OUT
~packing:hp#add () ~packing:hp#add ()
with Gtk.Error _ -> assert false with Gtk.Error _ -> assert false
let () = scrollview#set_shadow_type `ETCHED_OUT
let (_ : GtkSignal.id) = let (_ : GtkSignal.id) =
scrollview#misc#connect#size_allocate scrollview#misc#connect#size_allocate
~callback: ~callback:
...@@ -1125,11 +1133,10 @@ let right_hb = GPack.hbox ~packing:(right_vb#pack ~expand:false) () ...@@ -1125,11 +1133,10 @@ let right_hb = GPack.hbox ~packing:(right_vb#pack ~expand:false) ()
(* goal text view *) (* goal text view *)
(******************) (******************)
let scrolled_task_view = GBin.scrolled_window let scrolled_task_view =
~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC GBin.scrolled_window
~packing:vp#add () ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
~shadow_type:`ETCHED_OUT ~packing:vp#add ()
let () = scrolled_task_view#set_shadow_type `ETCHED_OUT
let (_ : GtkSignal.id) = let (_ : GtkSignal.id) =
scrolled_task_view#misc#connect#size_allocate scrolled_task_view#misc#connect#size_allocate
...@@ -1154,11 +1161,9 @@ let () = task_view#set_highlight_current_line true ...@@ -1154,11 +1161,9 @@ let () = task_view#set_highlight_current_line true
let scrolled_source_view = GBin.scrolled_window let scrolled_source_view = GBin.scrolled_window
~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
~packing:vp#add ~packing:vp#add ~shadow_type:`ETCHED_OUT
() ()
let () = scrolled_source_view#set_shadow_type `ETCHED_OUT
let source_view = let source_view =
GSourceView2.source_view GSourceView2.source_view
~auto_indent:true ~auto_indent:true
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment