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