diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 63bbcd3c9f4535fb2d4bce5a5ed485aaec8db6a4..550c62ee06f8db0572df32dd55ad9501e37b01a9 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -497,20 +497,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 -> ()
diff --git a/src/plugins/gui/wbox.ml b/src/plugins/gui/wbox.ml
index 593d2c11a6a2a80a7833e6895d25d18bf324a942..a00525e95e893cc36e7b9bfa9744eb98a11f75a7 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,17 @@ 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 ]
+
+let split ~dir ?get ?set 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
diff --git a/src/plugins/gui/wbox.mli b/src/plugins/gui/wbox.mli
index 3cf819eb36ac278f6a07af3f760c791c668f0e29..b0b3c142f4439a605b9f3c2b4b8aa5174a4b2c06 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,21 @@ 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
+val split :
+ dir:[`HORIZONTAL|`VERTICAL] ->
+ ?get:(unit -> float) ->
+ ?set:(float -> unit) ->
+ widget -> 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