From ebb6acf809127604fb6f33a7c0b9d23a054db3cd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 4 Mar 2019 10:46:13 +0100
Subject: [PATCH] [wp/gui] insert a splitter for palette
---
src/plugins/wp/GuiGoal.ml | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index 9ba3bf0cc94..eb3a8695830 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
--
GitLab