Merge branch 'feature/wp/fix-tip-gui' into 'master'

[WP/TIP] Adds a splitter to tactic palette

See merge request frama-c/frama-c!2185

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

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

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

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

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

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