diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 550c62ee06f8db0572df32dd55ad9501e37b01a9..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()))
@@ -713,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
@@ -859,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 -> ()
@@ -906,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 ());
@@ -1033,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 575431003da55661039bfcaf562aac8c86edebc1..b15c784631b9f3bf89f3100751e691eafc8a072c 100644
--- a/src/plugins/gui/wbox.ml
+++ b/src/plugins/gui/wbox.ml
@@ -97,19 +97,28 @@ let panel ?top ?left ?right ?bottom center =
| None , Some t -> vbox [ hv middle ; w t ]
| Some a , Some b -> vbox [ h a ; hv middle ; h b ]
-let split ~dir ?get ?set w1 w2 =
+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 ;
- begin match get with None -> () | Some fget ->
- Wutil.set_pane_ratio pane (fget())
- end ;
- begin match set with None -> () | Some fset ->
- let callback _ =
- fset (Wutil.get_pane_ratio pane) ; false in
- ignore (pane#event#connect#button_release ~callback) ;
- end ;
- new Wutil.gobj_widget pane
+ 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 =
let scrolled = GBin.scrolled_window ~vpolicy ~hpolicy () in
diff --git a/src/plugins/gui/wbox.mli b/src/plugins/gui/wbox.mli
index b9e2912d6c4889dd5a1b4dc1ffab5cacd05a8ea0..822f9641f9972e998ffef70491c17debeb1a194c 100644
--- a/src/plugins/gui/wbox.mli
+++ b/src/plugins/gui/wbox.mli
@@ -82,11 +82,17 @@ val sidebar : box list -> box list -> widget
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] ->
- ?get:(unit -> float) ->
- ?set:(float -> unit) ->
- widget -> widget -> widget
+ widget -> widget -> splitter
(** default policy is AUTOMATIC *)
val scroll: