[gui] add split pane utilities

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 -> ()
 

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

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

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                                                  --- *)
 (* -------------------------------------------------------------------------- *)

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