diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 63bbcd3c9f4535fb2d4bce5a5ed485aaec8db6a4..0c3551ccbb0663fc2a0859f8a2c8561377f999f7 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -121,6 +121,11 @@ module Configuration = struct
widget#set init ;
widget#connect (set_bool key)
+ let config_float ~key ~default widget =
+ let init = find_float ~default key in
+ widget#set init ;
+ widget#connect (set_float key)
+
let config_values ~key ~default ~values widget =
begin
let of_string s = fst (List.find (fun e -> snd e = s) values) in
@@ -366,7 +371,7 @@ let on_bool ?tooltip ?use_markup (container:GPack.box) label get set =
let container = GPack.hbox ~packing:container#pack () in
do_tooltip ?tooltip container;
let button =
- GButton.check_button ~packing:container#pack ~active:!result ()
+ GButton.check_button ~packing:container#pack ~active:!result ()
in
ignore (mk_label ?use_markup container ~xalign:0. label);
ignore (button#connect#toggled ~callback:(fun () -> set button#active));
@@ -428,7 +433,7 @@ let on_string ?tooltip ?use_markup ?(validator=(fun _ -> true)) ?width
ignore (entry#event#connect#focus_out ~callback);
ignore (entry#connect#activate ~callback:(fun () -> ignore (callback ())));
ignore (mk_label ?use_markup ~xalign:0. container label);
- (fun () ->
+ (fun () ->
if not (Gobject.Property.get entry#as_widget GtkBase.Widget.P.has_focus)
then entry#set_text (get ()))
@@ -440,7 +445,7 @@ let on_string_set ?tooltip ?use_markup ?width (container:GPack.box) label get se
ignore (entry#event#connect#focus_out ~callback);
ignore (entry#connect#activate ~callback:(fun () -> ignore (callback ())));
ignore (mk_label ?use_markup ~xalign:0. container (label ^ " (list)"));
- (fun () ->
+ (fun () ->
if not (Gobject.Property.get entry#as_widget GtkBase.Widget.P.has_focus)
then entry#set_text (get()))
@@ -497,20 +502,10 @@ let on_combo
(* ------------------------------------------------------------------------ *)
let save_paned_ratio key (paned:GPack.paned) =
- let paned_min_pos = paned#min_position in
- let paned_max_pos = paned#max_position in
- let length = paned_max_pos - paned_min_pos in
- let ratio = if length = 0 then 0.5
- else (float_of_int paned#position)/.(float_of_int length)
- in
+ let ratio = Wutil.get_pane_ratio paned in
Configuration.set key (Configuration.ConfFloat ratio)
-let place_paned (paned:GPack.paned) factor =
- let paned_min_pos = paned#min_position in
- let offset =
- int_of_float (float (paned#max_position - paned_min_pos)*.factor)
- in
- paned#set_position (paned_min_pos + offset)
+let place_paned = Wutil.set_pane_ratio
let old_gtk_compat f x = try f x with Not_found -> ()
@@ -723,7 +718,7 @@ class type host = object
method private set_reset: (unit -> unit) -> unit
end
-class error_manager ?reset (o_parent:GWindow.window_skel) : host =
+class error_manager ?reset (o_parent:GWindow.window_skel) : host =
object (self: #host)
val mutable f_reset = match reset with
@@ -869,11 +864,11 @@ let open_in_external_viewer ?(line=1) (file : Datatype.Filepath.t) =
ignore (Sys.command cmd)
exception Too_many_events
-let refresh_gui () =
+let refresh_gui () =
let counter = ref 0 in
- try
- while Glib.Main.iteration false do
- if !counter >= 10 then raise Too_many_events
+ try
+ while Glib.Main.iteration false do
+ if !counter >= 10 then raise Too_many_events
else incr counter
done
with Too_many_events -> ()
@@ -916,7 +911,7 @@ let source_files_chooser (main_ui: source_files_chooser_host) defaults f =
~packing:(hbox#pack ~expand:true ~fill:true)
()
in
- Configuration.use_string "last_opened_dir"
+ Configuration.use_string "last_opened_dir"
(fun s -> ignore (filechooser#set_current_folder s));
filechooser#set_select_multiple true;
filechooser#add_filter (accepted_source_files ());
@@ -1043,8 +1038,8 @@ let graph_window_through_dot ~parent ~title dot_formatter =
let fmt = Format.formatter_of_out_channel (open_out temp_file) in
dot_formatter fmt;
Format.pp_print_flush fmt ();
- let view =
- snd
+ let view =
+ snd
(Dgraph.DGraphContainer.Dot.from_dot_with_commands ~packing temp_file)
in
view
diff --git a/src/plugins/gui/gtk_helper.mli b/src/plugins/gui/gtk_helper.mli
index 37c82a18e9aa136c706fb35baa76c52a84bf370e..776e4d3560d974bb684e74186bb8489875709025 100644
--- a/src/plugins/gui/gtk_helper.mli
+++ b/src/plugins/gui/gtk_helper.mli
@@ -95,7 +95,7 @@ module Configuration: sig
val set_int: string -> int -> unit
(** Sets a ConfigInt *)
-
+
val find_bool : ?default:bool -> string -> bool
(** Same as {find_int}. *)
@@ -127,13 +127,13 @@ module Configuration: sig
(** Helpers to connect widgets to configuration values.
The configuration value is first pushed to the widget
using method [#set], or the [~default] value is used instead.
-
+
Then, a callback is registered
into the widget via [#connect] such that subsequent
- values from user's action are saved back into the
+ values from user's action are saved back into the
configuration file. *)
- (** Abstract interface to the connected widget.
+ (** Abstract interface to the connected widget.
This API is consistent with the [Widget] ones. *)
class type ['a] selector =
object
@@ -142,15 +142,16 @@ module Configuration: sig
method connect : ('a -> unit) -> unit
(** Register a callback invoked by the widget each time the value is edited. *)
end
-
+
val config_int : key:string -> default:int -> int #selector -> unit
val config_bool : key:string -> default:bool -> bool #selector -> unit
val config_string : key:string -> default:string -> string #selector -> unit
+ val config_float : key:string -> default:float -> float #selector -> unit
val config_values : key:string -> default:'a ->
values:('a * string) list -> 'a #selector -> unit
- (** The [values] field is used as a dictionary of available values.
+ (** The [values] field is used as a dictionary of available values.
They are compared with [Pervasives.(=)]. *)
-
+
end
(* ************************************************************************** *)
diff --git a/src/plugins/gui/wbox.ml b/src/plugins/gui/wbox.ml
index 593d2c11a6a2a80a7833e6895d25d18bf324a942..df6f6d122527fa15ff20294db9efd5f2a6034ec0 100644
--- a/src/plugins/gui/wbox.ml
+++ b/src/plugins/gui/wbox.ml
@@ -78,7 +78,7 @@ let vgroup (ws : widget list) =
let box = GPack.vbox ~show:true ~homogeneous:true () in
List.iter (fun w -> box#pack ~expand:false w#coerce) ws ;
new Wutil.gobj_widget box
-
+
let (<|>) xs ys = if ys = [] then xs else (xs @ (ToEnd::ys))
let toolbar xs ys = hbox (xs <|> ys)
@@ -96,3 +96,38 @@ let panel ?top ?left ?right ?bottom center =
| Some t , None -> vbox [ h t ; hv middle ]
| None , Some t -> vbox [ hv middle ; w t ]
| Some a , Some b -> vbox [ h a ; hv middle ; h b ]
+
+class type splitter =
+ object
+ inherit Wutil.widget
+ method get : float
+ method set : float -> unit
+ method connect : (float -> unit) -> unit
+ end
+
+let split ~dir w1 w2 =
+ let pane = GPack.paned dir () in
+ pane#add1 w1#coerce ;
+ pane#add2 w2#coerce ;
+ let splitter =
+ object
+ inherit (Wutil.gobj_widget pane)
+ method get = Wutil.get_pane_ratio pane
+ method set = Wutil.set_pane_ratio pane
+ method connect f =
+ let callback _ = f (Wutil.get_pane_ratio pane) ; false in
+ ignore (pane#event#connect#button_release ~callback)
+ end
+ in (splitter :> splitter)
+
+let scroll ?(hpolicy=`AUTOMATIC) ?(vpolicy=`AUTOMATIC) w =
+ (* Explicit conversion needed for lablgtk3, as policy_type has been extended
+ with another constructor but we still export the lablgtk2 type. *)
+ let vpolicy = (vpolicy :> Gtk.Tags.policy_type) in
+ let hpolicy = (hpolicy :> Gtk.Tags.policy_type) in
+ let scrolled = GBin.scrolled_window ~vpolicy ~hpolicy () in
+ scrolled#add_with_viewport w#coerce ;
+ new Wutil.gobj_widget scrolled
+
+let hscroll w = scroll ~vpolicy:`NEVER w
+let vscroll w = scroll ~hpolicy:`NEVER w
diff --git a/src/plugins/gui/wbox.mli b/src/plugins/gui/wbox.mli
index 3cf819eb36ac278f6a07af3f760c791c668f0e29..822f9641f9972e998ffef70491c17debeb1a194c 100644
--- a/src/plugins/gui/wbox.mli
+++ b/src/plugins/gui/wbox.mli
@@ -52,12 +52,12 @@ val label : ?fill:bool -> ?style:style -> ?align:align -> ?padding:int -> string
Default: [~fill:false ~style:`Label ~align:`Left ~padding:0] *)
-(** [hbox] and [vbox] can be used to created nested boxes.
- Typically, local scope opening can be used, typically:
+(** [hbox] and [vbox] can be used to created nested boxes.
+ Typically, local scope opening can be used, typically:
[Wbox.(hbox [ w A ; w B ; w C ])],
- where [A], [B] and [C] are widgets, or boxes.
+ where [A], [B] and [C] are widgets, or boxes.
- Notice that nested boxes can {i generally} be packed using default
+ Notice that nested boxes can {i generally} be packed using default
[W] mode, even if they contains horizontal or vertical widgets. *)
val hbox : box list -> widget (** Pack a list of boxes horizontally. *)
@@ -69,16 +69,39 @@ val hgroup : widget list -> widget
(** Pack a list of widgets vertically, with all widgets stuck to the same width *)
val vgroup : widget list -> widget
-(** The first list is packed to the left side of the toolbar.
+(** The first list is packed to the left side of the toolbar.
The second list is packed to the right side of the toolbar. *)
val toolbar : box list -> box list -> widget
-(** The first list is packed to the top of the sidebar.
+(** The first list is packed to the top of the sidebar.
The second list is packed to the bottom of the sidebar. *)
val sidebar : box list -> box list -> widget
(** Helper to create a full featured window:
- [~top] is layout as a toolbar, [left] and [right] as sidebars, and [bottom] as a status bar.
+ [~top] is layout as a toolbar, [left] and [right] as sidebars, and [bottom] as a status bar.
The main (non-optional) widget is centered with full expansion in both directions. *)
val panel : ?top:widget -> ?left:widget -> ?right:widget -> ?bottom:widget -> #widget -> widget
+class type splitter =
+ object
+ inherit Wutil.widget
+ method get : float
+ method set : float -> unit
+ method connect : (float -> unit) -> unit
+ end
+
+val split :
+ dir:[`HORIZONTAL|`VERTICAL] ->
+ widget -> widget -> splitter
+
+(** default policy is AUTOMATIC *)
+val scroll:
+ ?hpolicy:[`AUTOMATIC|`ALWAYS|`NEVER] ->
+ ?vpolicy:[`AUTOMATIC|`ALWAYS|`NEVER] ->
+ widget -> widget
+
+(** Same as [scroll ~vpolicy:`NEVER] *)
+val hscroll : widget -> widget
+
+(** Same as [scroll ~volicy:`NEVER] *)
+val vscroll : widget -> widget
diff --git a/src/plugins/gui/wutil.ml b/src/plugins/gui/wutil.ml
index 42ee0a7912af178d9047560d5c128b7d0b9efde8..7836b767e86b0f7c75531b592d0589318e1915bd 100644
--- a/src/plugins/gui/wutil.ml
+++ b/src/plugins/gui/wutil.ml
@@ -81,6 +81,23 @@ let later f =
let prio = Glib.int_of_priority `LOW in
ignore (Glib.Idle.add ~prio for_idle)
+(* -------------------------------------------------------------------------- *)
+(* --- Ratio --- *)
+(* -------------------------------------------------------------------------- *)
+
+let get_pane_ratio (paned:GPack.paned) =
+ let paned_min_pos = paned#min_position in
+ let paned_max_pos = paned#max_position in
+ let length = paned_max_pos - paned_min_pos in
+ if length = 0 then 0.5
+ else (float_of_int paned#position)/.(float_of_int length)
+
+let set_pane_ratio (paned:GPack.paned) ratio =
+ let paned_min_pos = paned#min_position in
+ let offset =
+ int_of_float (float (paned#max_position - paned_min_pos) *. ratio)
+ in paned#set_position (paned_min_pos + offset)
+
(* -------------------------------------------------------------------------- *)
(* --- Widget & Signals --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/gui/wutil.mli b/src/plugins/gui/wutil.mli
index aa07048eedd8128813b0655684314b569fed8b57..390967dbcb3295d6ab1e29fe74801eac34ee8b5c 100644
--- a/src/plugins/gui/wutil.mli
+++ b/src/plugins/gui/wutil.mli
@@ -43,6 +43,11 @@ val set_small_font : #GObj.widget -> unit
val set_bold_font : #GObj.widget -> unit
val to_utf8 : string -> string
+(** {2 Ratios} *)
+
+val get_pane_ratio : GPack.paned -> float
+val set_pane_ratio : GPack.paned -> float -> unit
+
(** {2 Timing} *)
val later : (unit -> unit) -> unit
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index 9ba3bf0cc946a7afb8a246f85e5c5817624d3900..eb3a8695830e41ff49a3fc8090ca11a6556844fe 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -82,12 +82,7 @@ class pane (proverpane : GuiConfig.provers) =
let composer = new GuiComposer.composer printer in
let browser = new GuiComposer.browser printer in
let layout = new Wutil.layout in
- let scroll_palette =
- GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`NEVER ()
- in
- let scroll_palette_widget = new Wutil.gobj_widget scroll_palette in
let palette = new Wpalette.panel () in
- let () = scroll_palette#add_with_viewport palette#coerce in
let help = new Widget.button
~label:"Tactics" ~border:false ~tooltip:"List Available Tactics" () in
let delete = new Widget.button
@@ -122,7 +117,12 @@ class pane (proverpane : GuiConfig.provers) =
w play_script ; w save_script ;
w ~padding:6 icon ; h ~padding:6 status ]
[ w help ; w delete ]) in
- layout#populate (Wbox.panel ~top:toolbar ~right:scroll_palette_widget text) ;
+ let content = Wbox.split ~dir:`HORIZONTAL
+ text#widget (Wbox.scroll palette#widget) in
+ Wutil.later (fun () ->
+ Config.config_float ~key:"GuiGoal.palette" ~default:0.8 content
+ );
+ layout#populate (Wbox.panel ~top:toolbar content#widget) ;
provers <-
VCS.([ new GuiProver.prover ~console:text ~prover:AltErgo ] @
List.map