diff --git a/.gitignore b/.gitignore index 7bb9b259fc6d8927b0ccc15288d70e617fae5b8a..7ec9d042239dfd18b32fbaa006ec67ec87fdce77 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 ab4b93aea0e2932900eedfd7baa3aa6a0a0c1747..bf039ac29c70eaf8b1040746560d4d3caeb41055 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 0000000000000000000000000000000000000000..b47503f29512771a27d3a478dd8f2dae5f2453f4 --- /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 0000000000000000000000000000000000000000..6592b261c24dd5f7eb843e1d11206228fbb018dc --- /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 0000000000000000000000000000000000000000..8352ffadc6c42a3ee25c8af3765396870b3d0046 --- /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 2c500414c7de604493f4902253b065d5d9bd9d2b..9879648c7143f2e9e77539c4ac9c139c0411baca 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 =