From aaf056cdc2b18a20b992ea5d2bc6b698685f8d58 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 10 Jan 2019 19:18:57 +0100
Subject: [PATCH] =?UTF-8?q?[gui]=20tame=20WP's=20feral=20=F0=9F=90=AF=20TI?=
=?UTF-8?q?P=20panel?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
And restore proper scrolling in all the other lower notebook items under gtk3
---
src/plugins/wp/GuiGoal.ml | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index 40d95b6abbc..5eb302348dd 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -74,7 +74,12 @@ 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 palette#coerce in
let help = new Widget.button
~label:"Tactics" ~border:false ~tooltip:"List Available Tactics" () in
let delete = new Widget.button
@@ -107,7 +112,7 @@ class pane (proverpane : GuiConfig.provers) =
w autofocus ; 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:palette#widget text) ;
+ layout#populate (Wbox.panel ~top:toolbar ~right:scroll_palette_widget text) ;
provers <-
VCS.([ new GuiProver.prover ~console:text ~prover:AltErgo ] @
List.map
--
GitLab