diff --git a/.gitignore b/.gitignore
index b23cad6d25f24614cf7673640cb83540327a888e..633a7d72b4f6a96980eec0d1d508467a17ddfa92 100644
--- a/.gitignore
+++ b/.gitignore
@@ -205,4 +205,3 @@ hello-*.tar.gz
/src/plugins/gui/GSourceView.ml
/src/plugins/gui/GSourceView.mli
/tests/crowbar/integer_bb_pretty
-/src/plugins/gui/pango_compat.ml
diff --git a/Makefile b/Makefile
index 2d95b71cd370b2b838a1f8bd7224d3083c11db93..9883857d274a05aa0f238c61c5062ee35edcde2f 100644
--- a/Makefile
+++ b/Makefile
@@ -725,23 +725,16 @@ ifeq ($(LABLGTK),lablgtk3)
src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.3.ml
$(CP) $< $@
$(CHMOD_RO) $@
-src/plugins/gui/pango_compat.ml: src/plugins/gui/pango_compat.3.ml
- $(CP) $< $@
- $(CHMOD_RO) $@
else
src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.2.ml
$(CP) $< $@
$(CHMOD_RO) $@
-src/plugins/gui/pango_compat.ml: src/plugins/gui/pango_compat.2.ml
- $(CP) $< $@
- $(CHMOD_RO) $@
endif
-GENERATED+=src/plugins/gui/gtk_compat.ml src/plugins/gui/pango_compat.ml
+GENERATED+=src/plugins/gui/gtk_compat.ml
SINGLE_GUI_CMO:= \
+ wutil_once \
gtk_compat \
- wutil_once \
- pango_compat \
$(WTOOLKIT) \
$(SOURCEVIEWCOMPAT) \
$(DGRAPHCOMPAT) \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 2322a5380b41ecb4fdcc404c19513f42013f92b3..dd34d6c7e782c8eb929528844e2b9d94027eb2d7 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -786,9 +786,6 @@ src/plugins/gui/launcher.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/launcher.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/menu_manager.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/menu_manager.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/pango_compat.2.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/pango_compat.3.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/pango_compat.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/pretty_source.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/pretty_source.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/project_manager.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/gui/gtk_compat.2.ml b/src/plugins/gui/gtk_compat.2.ml
index c81dea81252802950c7d1e464a7093c2ad3dc976..4bc1c0d776d4f419371dafbebfbc2c4689aaddcb 100644
--- a/src/plugins/gui/gtk_compat.2.ml
+++ b/src/plugins/gui/gtk_compat.2.ml
@@ -20,6 +20,27 @@
(* *)
(**************************************************************************)
+module Pango = struct
+ open Wutil_once
+
+ let small_font =
+ once (fun f ->
+ let f = Pango.Font.copy f in
+ let s = Pango.Font.get_size f in
+ Pango.Font.set_size f (s-2) ; f)
+
+ let bold_font =
+ once (fun f ->
+ let f = Pango.Font.copy f in
+ Pango.Font.set_weight f `BOLD ; f)
+
+ let modify_font phi widget =
+ widget#misc#modify_font (phi widget#misc#pango_context#font_description)
+
+ let set_small_font w = modify_font small_font w
+ let set_bold_font w = modify_font bold_font w
+end
+
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
index 92edbea64f8bf4c45279ac49d13e86ab4fd2e5a8..fecbc6508665e8660499df188b2e5a2065a3c046 100644
--- a/src/plugins/gui/gtk_compat.3.ml
+++ b/src/plugins/gui/gtk_compat.3.ml
@@ -20,6 +20,28 @@
(* *)
(**************************************************************************)
+module Pango = struct
+ open Wutil_once
+
+ let small_font =
+ once (fun (f: GPango.font_description) ->
+ let f = f#copy in
+ let size = f#size - 2 in
+ f#modify ~size (); f)
+
+ let bold_font =
+ once (fun (f: GPango.font_description) ->
+ let f = f#copy in
+ let weight = `BOLD in
+ f#modify ~weight (); f)
+
+ let modify_font phi (widget: #GObj.widget) =
+ widget#misc#modify_font (phi widget#misc#pango_context#font_description)
+
+ let set_small_font w = modify_font small_font w
+ let set_bold_font w = modify_font bold_font w
+end
+
let get_toolbar_index toolbar item = toolbar#get_item_index item#as_tool_item
let window = GWindow.window
diff --git a/src/plugins/gui/gtk_compat.mli b/src/plugins/gui/gtk_compat.mli
index 8a530fd2dd361d0b5aa424d344dba3059e251dfd..16f554231bdfd307259bf30aa0abf484cae3e769 100644
--- a/src/plugins/gui/gtk_compat.mli
+++ b/src/plugins/gui/gtk_compat.mli
@@ -20,6 +20,11 @@
(* *)
(**************************************************************************)
+module Pango : sig
+ val set_small_font : #GObj.widget -> unit (** makes the font smaller. *)
+ val set_bold_font : #GObj.widget -> unit (** makes the font bold. *)
+end
+
val get_toolbar_index: GButton.toolbar -> GButton.tool_item -> int
val window:
diff --git a/src/plugins/gui/pango_compat.2.ml b/src/plugins/gui/pango_compat.2.ml
deleted file mode 100644
index e19e316f9cda8accca60110b5f58681d39946bf9..0000000000000000000000000000000000000000
--- a/src/plugins/gui/pango_compat.2.ml
+++ /dev/null
@@ -1,42 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2019 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-include Wutil_once
-
-let small_font =
- once (fun f ->
- let f = Pango.Font.copy f in
- let s = Pango.Font.get_size f in
- Pango.Font.set_size f (s-2) ; f)
-
-let bold_font =
- once (fun f ->
- let f = Pango.Font.copy f in
- Pango.Font.set_weight f `BOLD ; f)
-
-let modify_font phi widget =
- widget#misc#modify_font (phi widget#misc#pango_context#font_description)
-
-let set_font w name = w#misc#modify_font_by_name name
-let set_monospace w = set_font w "monospace"
-let set_small_font w = modify_font small_font w
-let set_bold_font w = modify_font bold_font w
diff --git a/src/plugins/gui/pango_compat.3.ml b/src/plugins/gui/pango_compat.3.ml
deleted file mode 100644
index 5088fe11546ee8100416a0c6a38fd85495e908da..0000000000000000000000000000000000000000
--- a/src/plugins/gui/pango_compat.3.ml
+++ /dev/null
@@ -1,43 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2019 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-include Wutil_once
-
-let small_font =
- once (fun (f: GPango.font_description) ->
- let f = f#copy in
- let size = f#size - 2 in
- f#modify ~size (); f)
-
-let bold_font =
- once (fun (f: GPango.font_description) ->
- let f = f#copy in
- let weight = `BOLD in
- f#modify ~weight (); f)
-
-let modify_font phi (widget: #GObj.widget) =
- widget#misc#modify_font (phi widget#misc#pango_context#font_description)
-
-let set_font w name = w#misc#modify_font_by_name name
-let set_monospace w = set_font w "monospace"
-let set_small_font w = modify_font small_font w
-let set_bold_font w = modify_font bold_font w
diff --git a/src/plugins/gui/pango_compat.mli b/src/plugins/gui/pango_compat.mli
deleted file mode 100644
index 773304b260d767b76968da0c3733c2e9523e8f30..0000000000000000000000000000000000000000
--- a/src/plugins/gui/pango_compat.mli
+++ /dev/null
@@ -1,38 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2019 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(** pango-related functions whose implementation is dependent on
- the lablgtk version that is used. *)
-
-include module type of Wutil_once
-
-(** set the font used by the widget according to its name. *)
-val set_font : #GObj.widget -> string -> unit
-
-(** makes the widget use a monospace font. *)
-val set_monospace : #GObj.widget -> unit
-
-(** makes the font smaller. *)
-val set_small_font : #GObj.widget -> unit
-
-(** makes the font bold. *)
-val set_bold_font : #GObj.widget -> unit
diff --git a/src/plugins/gui/wutil.ml b/src/plugins/gui/wutil.ml
index 662657fde181fdbc815e250d53853814b928d072..42ee0a7912af178d9047560d5c128b7d0b9efde8 100644
--- a/src/plugins/gui/wutil.ml
+++ b/src/plugins/gui/wutil.ml
@@ -26,16 +26,21 @@
let on x f = match x with None -> () | Some x -> f x
let fire fs x = List.iter (fun f -> f x) fs
+let once = Wutil_once.once
(* -------------------------------------------------------------------------- *)
(* --- Pango Properties --- *)
(* -------------------------------------------------------------------------- *)
-include Pango_compat
+include Gtk_compat.Pango
+
+let set_font w name = w#misc#modify_font_by_name name
+let set_monospace w = set_font w "monospace"
(* -------------------------------------------------------------------------- *)
(* --- Misc --- *)
(* -------------------------------------------------------------------------- *)
+
let set_tooltip w m = on m w#misc#set_tooltip_text
let set_enabled (w : #GObj.widget) = w#misc#set_sensitive
let set_visible (w : #GObj.widget) e =
diff --git a/src/plugins/gui/wutil_once.ml b/src/plugins/gui/wutil_once.ml
index cadbd38e0ff46c26ad815d6a1390bd669e62f76c..415eda7ef37bd8d8f39f3fe47bc35e49dd143574 100644
--- a/src/plugins/gui/wutil_once.ml
+++ b/src/plugins/gui/wutil_once.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(* belongs to Wutil, but used by Pango_compat.{2,3}.ml *)
+(* belongs to Wutil, but used by gtk_compat.{2,3}.ml *)
type ('a,'b) cell = Value of 'b | Fun of ('a -> 'b)
let get p x =