From c6ffe22455ecdcf343fef8bebec844fd95ff1f4a 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:22:25 +0100
Subject: [PATCH] [gui] scroll utility
---
src/plugins/gui/wbox.ml | 8 ++++++++
src/plugins/gui/wbox.mli | 12 ++++++++++++
2 files changed, 20 insertions(+)
diff --git a/src/plugins/gui/wbox.ml b/src/plugins/gui/wbox.ml
index a00525e95e8..575431003da 100644
--- a/src/plugins/gui/wbox.ml
+++ b/src/plugins/gui/wbox.ml
@@ -110,3 +110,11 @@ let split ~dir ?get ?set w1 w2 =
ignore (pane#event#connect#button_release ~callback) ;
end ;
new Wutil.gobj_widget pane
+
+let scroll ?(hpolicy=`AUTOMATIC) ?(vpolicy=`AUTOMATIC) w =
+ 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
diff --git a/src/plugins/gui/wbox.mli b/src/plugins/gui/wbox.mli
index b0b3c142f44..b9e2912d6c4 100644
--- a/src/plugins/gui/wbox.mli
+++ b/src/plugins/gui/wbox.mli
@@ -87,3 +87,15 @@ val split :
?get:(unit -> float) ->
?set:(float -> unit) ->
widget -> widget -> widget
+
+(** 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
--
GitLab