[gui] compatibility with current lablgtk3 branch

.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

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) \

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

src/plugins/gui/pango_compat.2.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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

src/plugins/gui/pango_compat.3.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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

src/plugins/gui/pango_compat.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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

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 =

src/plugins/gui/wutil_once.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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))

src/plugins/gui/wutil_once.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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