From c1bd6622edbaf9af72da6d820cc296f291f08b66 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 3 Jan 2019 18:46:53 +0100
Subject: [PATCH] [gui] don't remove lablgtk2 compatibility too early
---
.gitignore | 1 +
Makefile | 12 ++++++++++++
src/plugins/gui/gtk_compat.2.ml | 2 ++
src/plugins/gui/gtk_compat.3.ml | 1 +
src/plugins/gui/gtk_compat.mli | 1 +
src/plugins/gui/menu_manager.ml | 5 ++++-
6 files changed, 21 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/gui/gtk_compat.2.ml
create mode 100644 src/plugins/gui/gtk_compat.3.ml
create mode 100644 src/plugins/gui/gtk_compat.mli
diff --git a/.gitignore b/.gitignore
index 7bb9b259fc6..7ec9d042239 100644
--- a/.gitignore
+++ b/.gitignore
@@ -201,3 +201,4 @@ hello-*.tar.gz
/src/plugins/gui/GSourceView2.ml
/src/plugins/gui/dgraph.ml
/src/plugins/gui/dgraph.mli
+/src/plugins/gui/gtk_compat.ml
diff --git a/Makefile b/Makefile
index ab4b93aea0e..bf039ac29c7 100644
--- a/Makefile
+++ b/Makefile
@@ -705,7 +705,19 @@ src/plugins/gui/dgraph.mli: src/plugins/gui/dgraph.mli.in
$(CHMOD_RO) $@
endif
+ifeq ($(LABLGTK),lablgtk3)
+src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.3.ml
+ $(CP) $< $@
+ $(CHMOD_RO) $@
+else
+src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.2.ml
+ $(CP) $< $@
+ $(CHMOD_RO) $@
+endif
+GENERATED+=src/plugins/gui/gtk_compat.ml
+
SINGLE_GUI_CMO:= \
+ gtk_compat \
$(WTOOLKIT) \
$(SOURCEVIEWCOMPAT) \
$(DGRAPHCOMPAT) \
diff --git a/src/plugins/gui/gtk_compat.2.ml b/src/plugins/gui/gtk_compat.2.ml
new file mode 100644
index 00000000000..b47503f2951
--- /dev/null
+++ b/src/plugins/gui/gtk_compat.2.ml
@@ -0,0 +1,2 @@
+let get_toolbar_index (toolbar:GButton.toolbar) (item:GButton.tool_item) =
+ toolbar#get_item_index item
diff --git a/src/plugins/gui/gtk_compat.3.ml b/src/plugins/gui/gtk_compat.3.ml
new file mode 100644
index 00000000000..6592b261c24
--- /dev/null
+++ b/src/plugins/gui/gtk_compat.3.ml
@@ -0,0 +1 @@
+let get_toolbar_index toolbar item = toolbar#get_item_index item#as_tool_item
diff --git a/src/plugins/gui/gtk_compat.mli b/src/plugins/gui/gtk_compat.mli
new file mode 100644
index 00000000000..8352ffadc6c
--- /dev/null
+++ b/src/plugins/gui/gtk_compat.mli
@@ -0,0 +1 @@
+val get_toolbar_index: GButton.toolbar -> GButton.tool_item -> int
diff --git a/src/plugins/gui/menu_manager.ml b/src/plugins/gui/menu_manager.ml
index 2c500414c7d..9879648c714 100644
--- a/src/plugins/gui/menu_manager.ml
+++ b/src/plugins/gui/menu_manager.ml
@@ -165,7 +165,10 @@ class menu_manager ?packing ~host:(_:Gtk_helper.host) =
By default, add all the others just before this very first group. *)
ref (match pos, first_tool_separator with
| None, None -> 0
- | None, Some sep -> max 0 (toolbar#get_item_index sep#as_tool_item)
+ | None, Some sep ->
+ max
+ 0
+ (Gtk_compat.get_toolbar_index toolbar (sep:>GButton.tool_item))
| Some p, _ -> p)
in
let toolbar_packing w =
--
GitLab