diff --git a/Makefile b/Makefile
index f88ac42621097efd24a58aeb773cec7e6ea0125a..9883857d274a05aa0f238c61c5062ee35edcde2f 100644
--- a/Makefile
+++ b/Makefile
@@ -733,6 +733,7 @@ endif
GENERATED+=src/plugins/gui/gtk_compat.ml
SINGLE_GUI_CMO:= \
+ wutil_once \
gtk_compat \
$(WTOOLKIT) \
$(SOURCEVIEWCOMPAT) \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index bd2f620f30888cf870d2a2fc03e33b986398352f..dd34d6c7e782c8eb929528844e2b9d94027eb2d7 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -814,6 +814,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/design.ml b/src/plugins/gui/design.ml
index f74d088be78e5ef2a0162a07066e06fb9962a167..1e8d0334f1ee83607308381926fe031e1cbf4aaa 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -842,17 +842,16 @@ class main_window () : main_window_extension_points =
width, if final_h then height else new_height
in
let main_window =
- GWindow.window
+ Gtk_compat.window
?icon:framac_icon
~title:"Frama-C"
- ~width
- ~height
~position:`CENTER
~resizable:true
~show:false
()
in
let () = main_window#set_default_size ~width ~height in
+ let () = main_window#set_geometry_hints ~min_size:(1,1) main_window#coerce in
let watch_cursor = Gdk.Cursor.create `WATCH in
let arrow_cursor = Gdk.Cursor.create `ARROW in
diff --git a/src/plugins/gui/gtk_compat.2.ml b/src/plugins/gui/gtk_compat.2.ml
index 945c310aa97880c02aa80cec3c2bd9b35f1da11b..4bc1c0d776d4f419371dafbebfbc2c4689aaddcb 100644
--- a/src/plugins/gui/gtk_compat.2.ml
+++ b/src/plugins/gui/gtk_compat.2.ml
@@ -20,5 +20,55 @@
(* *)
(**************************************************************************)
+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
+
+let window
+ ?(kind:Gtk.Tags.window_type option)
+ ?(title:string option)
+ ?(decorated:bool option)
+ ?(deletable:bool option)
+ ?(focus_on_map:bool option)
+ ?(icon:GdkPixbuf.pixbuf option)
+ ?(icon_name:string option)
+ ?(modal:bool option)
+ ?(position:Gtk.Tags.window_position option)
+ ?(resizable:bool option)
+ ?(screen:Gdk.screen option)
+ ?(type_hint:Gdk.Tags.window_type_hint option)
+ ?(urgency_hint:bool option)
+ ?(wmclass:(string * string) option)
+ ?(border_width:int option)
+ ?(width:int option)
+ ?(height:int option)
+ ?(show:bool option)
+ ()
+ =
+ let allow_shrink = resizable in
+ let allow_grow = resizable in
+ ignore wmclass;
+ GWindow.window
+ ?kind ?title ?decorated ?deletable ?focus_on_map ?icon ?icon_name
+ ?modal ?position ?resizable ?allow_grow ?allow_shrink ?screen
+ ?type_hint ?urgency_hint ?border_width ?width ?height ?show ()
diff --git a/src/plugins/gui/gtk_compat.3.ml b/src/plugins/gui/gtk_compat.3.ml
index b29fa610143511694a30dbd7a1358e153bbafeb6..fecbc6508665e8660499df188b2e5a2065a3c046 100644
--- a/src/plugins/gui/gtk_compat.3.ml
+++ b/src/plugins/gui/gtk_compat.3.ml
@@ -20,4 +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 61f6af64a07b6d382d0fb836b8f19b96049280dc..16f554231bdfd307259bf30aa0abf484cae3e769 100644
--- a/src/plugins/gui/gtk_compat.mli
+++ b/src/plugins/gui/gtk_compat.mli
@@ -20,4 +20,27 @@
(* *)
(**************************************************************************)
+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:
+ ?kind:Gtk.Tags.window_type ->
+ ?title:string ->
+ ?decorated:bool ->
+ ?deletable:bool ->
+ ?focus_on_map:bool ->
+ ?icon:GdkPixbuf.pixbuf ->
+ ?icon_name:string ->
+ ?modal:bool ->
+ ?position:Gtk.Tags.window_position ->
+ ?resizable:bool ->
+ ?screen:Gdk.screen ->
+ ?type_hint:Gdk.Tags.window_type_hint ->
+ ?urgency_hint:bool ->
+ ?wmclass:(string * string) ->
+ ?border_width:int ->
+ ?width:int -> ?height:int -> ?show:bool -> unit -> GWindow.window
diff --git a/src/plugins/gui/wutil.ml b/src/plugins/gui/wutil.ml
index 64421cb491ca77aab6056815a257086b0a8d803f..42ee0a7912af178d9047560d5c128b7d0b9efde8 100644
--- a/src/plugins/gui/wutil.ml
+++ b/src/plugins/gui/wutil.ml
@@ -26,36 +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
-
-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))
+let once = Wutil_once.once
(* -------------------------------------------------------------------------- *)
(* --- 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 Gtk_compat.Pango
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..415eda7ef37bd8d8f39f3fe47bc35e49dd143574
--- /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 gtk_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