diff --git a/.gitignore b/.gitignore
index 633a7d72b4f6a96980eec0d1d508467a17ddfa92..b23cad6d25f24614cf7673640cb83540327a888e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -205,3 +205,4 @@ 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 f88ac42621097efd24a58aeb773cec7e6ea0125a..2d95b71cd370b2b838a1f8bd7224d3083c11db93 100644
--- a/Makefile
+++ b/Makefile
@@ -725,15 +725,23 @@ 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
+GENERATED+=src/plugins/gui/gtk_compat.ml src/plugins/gui/pango_compat.ml
SINGLE_GUI_CMO:= \
gtk_compat \
+ wutil_once \
+ pango_compat \
$(WTOOLKIT) \
$(SOURCEVIEWCOMPAT) \
$(DGRAPHCOMPAT) \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index bd2f620f30888cf870d2a2fc03e33b986398352f..2322a5380b41ecb4fdcc404c19513f42013f92b3 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -786,6 +786,9 @@ 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
@@ -814,6 +817,8 @@ src/plugins/gui/wtext.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/wtext.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/wutil.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/wutil.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/wutil_once.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/wutil_once.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/impact/Impact.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/impact/compute_impact.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/impact/compute_impact.mli: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/gui/pango_compat.2.ml b/src/plugins/gui/pango_compat.2.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e19e316f9cda8accca60110b5f58681d39946bf9
--- /dev/null
+++ b/src/plugins/gui/pango_compat.2.ml
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(* *)
+(* 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
new file mode 100644
index 0000000000000000000000000000000000000000..5088fe11546ee8100416a0c6a38fd85495e908da
--- /dev/null
+++ b/src/plugins/gui/pango_compat.3.ml
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(* *)
+(* 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
new file mode 100644
index 0000000000000000000000000000000000000000..773304b260d767b76968da0c3733c2e9523e8f30
--- /dev/null
+++ b/src/plugins/gui/pango_compat.mli
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(* *)
+(* 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 64421cb491ca77aab6056815a257086b0a8d803f..662657fde181fdbc815e250d53853814b928d072 100644
--- a/src/plugins/gui/wutil.ml
+++ b/src/plugins/gui/wutil.ml
@@ -27,35 +27,15 @@
let on x f = match x with None -> () | Some x -> f x
let fire fs x = List.iter (fun f -> f x) fs
-type ('a,'b) cell = Value of 'b | Fun of ('a -> 'b)
-let get p x =
- match !p with
- | Value y -> y
- | Fun f -> let y = f x in p := Value y ; y
-let once f = get (ref (Fun f))
-
(* -------------------------------------------------------------------------- *)
(* --- Pango Properties --- *)
(* -------------------------------------------------------------------------- *)
-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)
+include Pango_compat
-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
+(* -------------------------------------------------------------------------- *)
+(* --- 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
new file mode 100644
index 0000000000000000000000000000000000000000..cadbd38e0ff46c26ad815d6a1390bd669e62f76c
--- /dev/null
+++ b/src/plugins/gui/wutil_once.ml
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* belongs to Wutil, but used by Pango_compat.{2,3}.ml *)
+
+type ('a,'b) cell = Value of 'b | Fun of ('a -> 'b)
+let get p x =
+ match !p with
+ | Value y -> y
+ | Fun f -> let y = f x in p := Value y ; y
+let once f = get (ref (Fun f))
diff --git a/src/plugins/gui/wutil_once.mli b/src/plugins/gui/wutil_once.mli
new file mode 100644
index 0000000000000000000000000000000000000000..60f48dded34de27016d132e4f0e2c51b5e64f9e7
--- /dev/null
+++ b/src/plugins/gui/wutil_once.mli
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** [once f] returns a function that will only be applied once per
+ execution of the program and returns the same value afterwards. *)
+val once: ('a -> 'b) -> 'a -> 'b