From 42a0c264b4f4e4f4069f0ac2a94234b3509718b4 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <tiky.halbaroth@gmail.com>
Date: Fri, 1 Jul 2022 00:04:28 +0200
Subject: [PATCH 1/6] Migrate Alt-Ergo from lablgtk2 to lablgtk3.

After this commit, the AltGr-Ergo package depends on lablgtk3 and
lablgtk3-sourcview3 packages.

Since GtkFontChooserDialog is not supported in lalbgtk3,
changing font in the editor is temporarily disabled.
---
 altgr-ergo.opam              |   4 +-
 dune-project                 |   4 +-
 src/bin/gui/annoted_ast.ml   |  81 ++++++----------
 src/bin/gui/annoted_ast.mli  |  16 ++--
 src/bin/gui/connected_ast.ml |  45 +++++----
 src/bin/gui/dune             |   4 +-
 src/bin/gui/gui_config.ml    |  27 +++---
 src/bin/gui/gui_config.mli   |   9 +-
 src/bin/gui/gui_util.ml      |  34 +++++++
 src/bin/gui/gui_util.mli     |  33 +++++++
 src/bin/gui/main_gui.ml      | 176 +++++++++++++++--------------------
 11 files changed, 225 insertions(+), 208 deletions(-)
 create mode 100644 src/bin/gui/gui_util.ml
 create mode 100644 src/bin/gui/gui_util.mli

diff --git a/altgr-ergo.opam b/altgr-ergo.opam
index 496ae843b..f96f57164 100644
--- a/altgr-ergo.opam
+++ b/altgr-ergo.opam
@@ -18,8 +18,8 @@ depends: [
   "dune" {>= "2.0" & < "3.0"}
   "alt-ergo-lib" {= version}
   "alt-ergo-parsers" {= version}
-  "lablgtk"
-  "conf-gtksourceview"
+  "lablgtk3"
+  "conf-gtksourceview3"
   "cmdliner" {>= "1.1.0"}
   "odoc" {with-doc}
 ]
diff --git a/dune-project b/dune-project
index cc5d947c3..6e01731fe 100644
--- a/dune-project
+++ b/dune-project
@@ -54,8 +54,8 @@ See more details on https://alt-ergo.ocamlpro.com/"
   (dune (and (>= 2.0) (< 3.0)))
   (alt-ergo-lib (= :version))
   (alt-ergo-parsers (= :version))
-  lablgtk
-  conf-gtksourceview
+  lablgtk3
+  conf-gtksourceview3
   (cmdliner (>= 1.1.0))
   (odoc :with-doc)
 )
diff --git a/src/bin/gui/annoted_ast.ml b/src/bin/gui/annoted_ast.ml
index 08fd7eec8..709cb9a75 100644
--- a/src/bin/gui/annoted_ast.ml
+++ b/src/bin/gui/annoted_ast.ml
@@ -35,14 +35,13 @@ open Options
 open Gui_config
 open Gui_session
 
-let monospace_font = Pango.Font.from_string monospace_font
-let general_font = Pango.Font.from_string general_font
-
+let font = GPango.font_description_from_string (font_family ^ " " ^ (string_of_int font_size))
+let font_size = font#size
 
 let make_indent nb =
-  String.make (min max_indent (nb * indent_size)) ' '
+  String.make (min max_indent (nb * indent_size)) ' ' 
 
-type sbuffer = GSourceView2.source_buffer
+type sbuffer = GSourceView3.source_buffer
 
 type error_model = {
   mutable some : bool;
@@ -203,9 +202,9 @@ module MTag = Map.Make (struct
 
 type env = {
   buffer : sbuffer;
-  goal_view : GSourceView2.source_view;
+  goal_view : GSourceView3.source_view;
   inst_buffer : sbuffer;
-  inst_view : GSourceView2.source_view;
+  inst_view : GSourceView3.source_view;
   errors : error_model;
   insts : inst_model;
   st_ctx : GMisc.statusbar_context;
@@ -229,53 +228,31 @@ module HTag = Hashtbl.Make (struct
     let hash t = t#get_oid
   end)
 
-
-
-
-let increase_size envs =
-  Pango.Font.set_size monospace_font
-    (Pango.Font.get_size monospace_font + 2000);
-  (* Printer.print_dbg "%d +" (Pango.Font.get_size monospace_font); *)
+let set_font ?(family=font#family) ?(size=font#size) ?(ratio=1.) () =
+  let new_sz = int_of_float ((float_of_int size) *. ratio) in
+  font#modify ~family:family ~size:new_sz ();
+  Gui_config.update_font_family font#family;
+  Gui_config.update_font_size font#size
+  
+let update_font envs =
   List.iter (fun env ->
-      env.goal_view#misc#modify_font monospace_font;
-      env.inst_view#misc#modify_font monospace_font;
-    ) envs;
-  Gui_config.update_monospace_font (Pango.Font.to_string monospace_font)
-
+      env.goal_view#misc#modify_font font;
+      env.inst_view#misc#modify_font font) envs
+  
+let increase_size envs =
+  set_font ~ratio:1.1 ();
+  (* Printer.print_dbg "Increase font size: %d" font#size; *)
+  update_font envs
 
 let decrease_size envs =
-  (* Printer.print_dbg "%d +" (Pango.Font.get_size monospace_font); *)
-  Pango.Font.set_size monospace_font
-    (Pango.Font.get_size monospace_font - 2000);
-  List.iter (fun env ->
-      env.goal_view#misc#modify_font monospace_font;
-      env.inst_view#misc#modify_font monospace_font;
-    ) envs;
-  Gui_config.update_monospace_font (Pango.Font.to_string monospace_font)
-
+  set_font ~ratio:0.9 ();
+  (* Printer.print_dbg "Decrease font size: %d" font#size; *)
+  update_font envs
 
 let reset_size envs =
-  Pango.Font.set_size monospace_font
-    (Pango.Font.get_size
-       (Pango.Font.from_string Gui_config.monospace_font));
-  List.iter (fun env ->
-      env.goal_view#misc#modify_font monospace_font;
-      env.inst_view#misc#modify_font monospace_font;
-    ) envs;
-  Gui_config.update_monospace_font (Pango.Font.to_string monospace_font)
-
-
-
-let set_font envs font =
-  let f = Pango.Font.from_string font in
-  Pango.Font.set_family monospace_font (Pango.Font.get_family f);
-  Pango.Font.set_size monospace_font (Pango.Font.get_size f);
-  List.iter (fun env ->
-      env.goal_view#misc#modify_font monospace_font;
-      env.inst_view#misc#modify_font monospace_font;
-    ) envs;
-  Gui_config.update_monospace_font (Pango.Font.to_string monospace_font)
-
+  set_font ~size: font_size ();
+  (* Printer.print_dbg "Reset font size: %d" font#size; *)
+  update_font envs
 
 type buffer_pending = {
   tags_ranges : ((sbuffer * int * int) list) HTag.t;
@@ -364,9 +341,9 @@ let create_env buf1 tv1 (buf2:sbuffer) tv2 errors insts st_ctx ast dep
 let create_replay_env buf1 errors insts ast actions resulting_ids =
   {
     buffer = buf1;
-    inst_buffer = GSourceView2.source_buffer ();
-    goal_view = GSourceView2.source_view ();
-    inst_view = GSourceView2.source_view ();
+    inst_buffer = GSourceView3.source_buffer ();
+    goal_view = GSourceView3.source_view ();
+    inst_view = GSourceView3.source_view ();
     errors = errors;
     insts = insts;
     st_ctx = (GMisc.statusbar ())#new_context ~name:"";
diff --git a/src/bin/gui/annoted_ast.mli b/src/bin/gui/annoted_ast.mli
index 6582ab2f5..378915e58 100644
--- a/src/bin/gui/annoted_ast.mli
+++ b/src/bin/gui/annoted_ast.mli
@@ -31,7 +31,7 @@ open Parsed
 open Typed
 open Gui_session
 
-type sbuffer = GSourceView2.source_buffer
+type sbuffer = GSourceView3.source_buffer
 
 type error_model = {
   mutable some : bool;
@@ -182,9 +182,9 @@ module MTag : Map.S with type key = GText.tag
 
 type env = {
   buffer : sbuffer;
-  goal_view : GSourceView2.source_view;
+  goal_view : GSourceView3.source_view;
   inst_buffer : sbuffer;
-  inst_view : GSourceView2.source_view;
+  inst_view : GSourceView3.source_view;
   errors : error_model;
   insts : inst_model;
   st_ctx : GMisc.statusbar_context;
@@ -202,21 +202,19 @@ type env = {
   resulting_ids : (string * int) list;
 }
 
-val monospace_font : Pango.font_description
-val general_font : Pango.font_description
-
+val font : GPango.font_description
 
 val increase_size : env list -> unit
 val decrease_size : env list -> unit
 val reset_size : env list -> unit
-val set_font : env list -> string -> unit
+val set_font : ?family:string -> ?size:int -> ?ratio:float -> unit -> unit
 
 
 val create_env :
   sbuffer ->
-  GSourceView2.source_view ->
+  GSourceView3.source_view ->
   sbuffer ->
-  GSourceView2.source_view ->
+  GSourceView3.source_view ->
   error_model ->
   inst_model ->
   GMisc.statusbar_context ->
diff --git a/src/bin/gui/connected_ast.ml b/src/bin/gui/connected_ast.ml
index 2f4177cc5..29feed4af 100644
--- a/src/bin/gui/connected_ast.ml
+++ b/src/bin/gui/connected_ast.ml
@@ -598,13 +598,12 @@ and add_instance ?(register=true) env id af ax_kd aname entries =
 and popup_axiom t env _offset () =
   let pop_w = GWindow.dialog
       ~title:"Instantiate axiom"
-      ~allow_grow:true
       ~position:`MOUSE
       ~width:400 ()
       (* ~icon:(GdkPixbuf.from_xpm_data Logo.xpm_logo) ()  *)
   in
   let bbox = GPack.button_box `HORIZONTAL ~border_width:5 ~layout:`END
-      ~child_height:20 ~child_width:85 ~spacing:10
+               ~spacing:10
       ~packing:pop_w#action_area#add () in
 
   let button_ok = GButton.button ~packing:bbox#add () in
@@ -692,10 +691,11 @@ and axiom_callback t env ~origin:y z i =
         let z = GdkEvent.Button.cast z in
         if GdkEvent.Button.button z = 3 then
           let menu = GMenu.menu () in
-          let image = GMisc.image ~stock:`ADD () in
-          let menuitem = GMenu.image_menu_item ~image
-              ~label:"Instanciate axiom ..." ~packing:menu#append () in
-          ignore(menuitem#connect#activate
+          let menu_item = GMenu.menu_item ~packing:menu#append () in
+          let vbox = GPack.hbox ~packing:menu_item#add () in
+          let _ = GMisc.label ~text:"Instanciate axiom ..." ~packing:vbox#add () in
+          let _ = GMisc.image ~stock:`ADD ~icon_size:`MENU ~packing:vbox#add () in
+          ignore(menu_item#connect#activate
                    ~callback:(popup_axiom t env offset));
           menu#popup ~button:3 ~time:(GdkEvent.Button.time z);
           true
@@ -753,13 +753,12 @@ and readd_trigger ?(register=true) env id str inst_buf =
 and popup_trigger t qid env (sbuf:sbuffer) offset () =
   let pop_w = GWindow.dialog
       ~title:"Add new (multi) trigger"
-      ~allow_grow:true
       ~width:400
       ~height:100 ()
       (* ~icon:(GdkPixbuf.from_xpm_data Logo.xpm_logo) ()  *)
   in
   let bbox = GPack.button_box `HORIZONTAL ~border_width:5 ~layout:`END
-      ~child_height:20 ~child_width:85 ~spacing:10
+               ~spacing:10
       ~packing:pop_w#action_area#add () in
 
   let button_ok = GButton.button ~packing:bbox#add () in
@@ -772,20 +771,20 @@ and popup_trigger t qid env (sbuf:sbuffer) offset () =
   ignore(GMisc.image ~stock:`CANCEL ~packing:phbox#add ());
   ignore(GMisc.label ~text:"Cancel" ~packing:phbox#add ());
 
-  let lmanager = GSourceView2.source_language_manager ~default:true in
+  let lmanager = GSourceView3.source_language_manager ~default:true in
   let source_language = lmanager#language "alt-ergo" in
   let buf1 = match source_language with
     | Some language ->
-      GSourceView2.source_buffer ~language
+      GSourceView3.source_buffer ~language
         ~highlight_syntax:true ~highlight_matching_brackets:true ()
-    | None -> GSourceView2.source_buffer () in
+    | None -> GSourceView3.source_buffer () in
   let sw1 = GBin.scrolled_window
       ~vpolicy:`AUTOMATIC
       ~hpolicy:`AUTOMATIC
       ~packing:pop_w#vbox#add () in
-  let tv1 = GSourceView2.source_view ~source_buffer:buf1 ~packing:(sw1#add)
-      ~show_line_numbers:true ~wrap_mode:`CHAR() in
-  let _ = tv1#misc#modify_font monospace_font in
+  let tv1 = GSourceView3.source_view ~source_buffer:buf1 ~packing:(sw1#add)
+              ~show_line_numbers:true ~wrap_mode:`CHAR() in
+  let _ = tv1#misc#modify_font font in
   let _ = tv1#set_editable true in
 
   let errors_l = GMisc.label ~text:"" ~packing:pop_w#vbox#pack () in
@@ -819,10 +818,11 @@ and triggers_callback t qid env sbuf ~origin:y z i =
         let z = GdkEvent.Button.cast z in
         if GdkEvent.Button.button z = 3 then
           let menu = GMenu.menu () in
-          let image = GMisc.image ~stock:`ADD () in
-          let menuitem = GMenu.image_menu_item ~image
-              ~label:"Add trigger(s) ..." ~packing:menu#append () in
-          ignore(menuitem#connect#activate
+          let menu_item = GMenu.menu_item ~packing:menu#append () in
+          let vbox = GPack.hbox ~packing:menu_item#add () in
+          let _ = GMisc.label ~text:"Add trigger(s) ..." ~packing:vbox#add () in
+          let _ = GMisc.image ~stock:`ADD ~icon_size:`MENU ~packing:vbox#add () in    
+          ignore(menu_item#connect#activate
                    ~callback:(popup_trigger t qid env sbuf offset));
           menu#popup ~button:3 ~time:(GdkEvent.Button.time z);
           true
@@ -965,20 +965,19 @@ let clear_used_lemmas_tags env =
   env.proof_toptags <- []
 
 let show_used_lemmas env expl =
-  let colormap = Gdk.Color.get_system_colormap () in
   let atags,ftags = findtags_proof expl env.ast in
   clear_used_lemmas_tags env;
   let max_mul = MTag.fold (fun _ m acc -> max acc m) ftags 0 in
   let green_0 =
-    Gdk.Color.alloc ~colormap (`RGB (65535*3/4, 65535, 65535*3/4))
+    Gdk.Color.color_parse (Gui_util.dec_to_hex_color (65535*3/4) 65535 (65535*3/4))
   in
   List.iter (fun t -> t#set_property (`BACKGROUND_GDK green_0)) atags;
   MTag.iter (fun t m ->
       let perc = ((max_mul - m) * 65535) / max_mul in
-      let green_n = Gdk.Color.alloc ~colormap
-          (`RGB (perc*1/2, (perc + 2*65535) /3, perc*1/2)) in
+      let green_n = Gdk.Color.color_parse
+          (Gui_util.dec_to_hex_color (perc*1/2) ((perc + 2*65535) /3) (perc*1/2)) in
       t#set_property (`BACKGROUND_GDK green_n)) ftags;
-  env.proof_tags <- ftags;
+  env.proof_tags <- ftags; 
   env.proof_toptags <- atags
 
 
diff --git a/src/bin/gui/dune b/src/bin/gui/dune
index 404eae99c..6272f0387 100644
--- a/src/bin/gui/dune
+++ b/src/bin/gui/dune
@@ -7,8 +7,8 @@
   (name         Main_gui)
   (public_name  altgr-ergo)
   (package      altgr-ergo)
-  (libraries    alt_ergo_common threads.posix lablgtk2 lablgtk2.sourceview2)
-  (modules      Gui_session Gui_config Annoted_ast Connected_ast
+  (libraries    alt_ergo_common threads.posix lablgtk3 lablgtk3-sourceview3)
+  (modules      Gui_util Gui_session Gui_config Annoted_ast Connected_ast
                 Gui_replay Main_gui)
   (link_flags   (-linkall))
 )
diff --git a/src/bin/gui/gui_config.ml b/src/bin/gui/gui_config.ml
index e0ae02c01..59b7b51c4 100644
--- a/src/bin/gui/gui_config.ml
+++ b/src/bin/gui/gui_config.ml
@@ -44,8 +44,8 @@ let window_height = ref 700
 let indent_size = ref 2
 let max_indent = ref 80
 let max_indents = ref 15
-let monospace_font = ref "monospace"
-let general_font = ref "sans"
+let font_family = ref "monospace"
+let font_size = ref 11
 let style = ref "tango"
 let wrap = ref false
 
@@ -63,10 +63,10 @@ let load () =
         max_indent := int_of_string value
       | [ "max_indents"; value ] ->
         max_indents := int_of_string value
-      | [ "monospace_font"; value ] ->
-        monospace_font := value
-      | [ "general_font"; value ] ->
-        general_font := value
+      | [ "font_family"; value ] ->
+        font_family := value
+      | [ "font_size"; value ] ->
+        font_size := int_of_string value
       | [ "style"; value ] ->
         style := value
       | [ "wrap"; value ] ->
@@ -85,8 +85,8 @@ let write () =
   output_string oc (sprintf "indent_size:%d\n" !indent_size);
   output_string oc (sprintf "max_indent:%d\n" !max_indent);
   output_string oc (sprintf "max_indents:%d\n" !max_indents);
-  output_string oc (sprintf "monospace_font:%s\n" !monospace_font);
-  output_string oc (sprintf "general_font:%s\n" !general_font);
+  output_string oc (sprintf "font_family:%s\n" !font_family);
+  output_string oc (sprintf "font_size:%s\n" (string_of_int !font_size));
   output_string oc (sprintf "style:%s\n" !style);
   output_string oc (sprintf "wrap:%b\n" !wrap);
   close_out oc
@@ -94,9 +94,12 @@ let write () =
 let update_window_size width height =
   window_width := width;
   window_height := height
+ 
+let update_font_family family =
+  font_family := family
 
-let update_monospace_font desc =
-  monospace_font := desc
+let update_font_size size =
+  font_size := size
 
 let update_wrap b =
   wrap := b
@@ -111,8 +114,8 @@ let window_height = !window_height
 let indent_size = !indent_size
 let max_indent = !max_indent
 let max_indents = !max_indents
-let monospace_font = !monospace_font
-let general_font = !general_font
+let font_family = !font_family
+let font_size = !font_size
 let style = !style
 let wrap = !wrap
 
diff --git a/src/bin/gui/gui_config.mli b/src/bin/gui/gui_config.mli
index 0e76439e5..554ee30ce 100644
--- a/src/bin/gui/gui_config.mli
+++ b/src/bin/gui/gui_config.mli
@@ -31,8 +31,8 @@ val window_height : int
 val indent_size : int
 val max_indent : int
 val max_indents : int
-val monospace_font : string
-val general_font : string
+val font_family : string
+val font_size : int
 val style : string
 val wrap : bool
 
@@ -50,7 +50,10 @@ val init : unit -> unit
 val update_window_size : int -> int -> unit
 
 (** Update the monospace font *)
-val update_monospace_font : string -> unit
+val update_font_family : string -> unit
+
+(** Update the font size *)
+val update_font_size : int -> unit
 
 val update_wrap : bool -> unit
 
diff --git a/src/bin/gui/gui_util.ml b/src/bin/gui/gui_util.ml
new file mode 100644
index 000000000..f553cc194
--- /dev/null
+++ b/src/bin/gui/gui_util.ml
@@ -0,0 +1,34 @@
+(******************************************************************************)
+(*                                                                            *)
+(*     The Alt-Ergo theorem prover                                            *)
+(*     Copyright (C) 2006-2022                                                *)
+(*                                                                            *)
+(*     Sylvain Conchon                                                        *)
+(*     Evelyne Contejean                                                      *)
+(*                                                                            *)
+(*     Francois Bobot                                                         *)
+(*     Mohamed Iguernelala                                                    *)
+(*     Stephane Lescuyer                                                      *)
+(*     Alain Mebsout                                                          *)
+(*     Pierre Villemot                                                        *)
+(*                                                                            *)
+(*     CNRS - INRIA - Universite Paris Sud                                    *)
+(*                                                                            *)
+(*     This file is distributed under the terms of the Apache Software        *)
+(*     License version 2.0                                                    *)
+(*                                                                            *)
+(*  ------------------------------------------------------------------------  *)
+(*                                                                            *)
+(*     Alt-Ergo: The SMT Solver For Software Verification                     *)
+(*     Copyright (C) 2013-2018 --- OCamlPro SAS                               *)
+(*                                                                            *)
+(*     This file is distributed under the terms of the Apache Software        *)
+(*     License version 2.0                                                    *)
+(*                                                                            *)
+(******************************************************************************)
+
+let dec_to_hex_color red green blue =
+  let r = Printf.sprintf "%04x" red in
+  let g = Printf.sprintf "%04x" green in
+  let b = Printf.sprintf "%04x" blue in
+  "#" ^ r ^ g ^ b
diff --git a/src/bin/gui/gui_util.mli b/src/bin/gui/gui_util.mli
new file mode 100644
index 000000000..5fdc4a349
--- /dev/null
+++ b/src/bin/gui/gui_util.mli
@@ -0,0 +1,33 @@
+(******************************************************************************)
+(*                                                                            *)
+(*     The Alt-Ergo theorem prover                                            *)
+(*     Copyright (C) 2006-2022                                                *)
+(*                                                                            *)
+(*     Sylvain Conchon                                                        *)
+(*     Evelyne Contejean                                                      *)
+(*                                                                            *)
+(*     Francois Bobot                                                         *)
+(*     Mohamed Iguernelala                                                    *)
+(*     Stephane Lescuyer                                                      *)
+(*     Alain Mebsout                                                          *)
+(*     Pierre Villemot                                                        *)
+(*                                                                            *)
+(*     CNRS - INRIA - Universite Paris Sud                                    *)
+(*                                                                            *)
+(*     This file is distributed under the terms of the Apache Software        *)
+(*     License version 2.0                                                    *)
+(*                                                                            *)
+(*  ------------------------------------------------------------------------  *)
+(*                                                                            *)
+(*     Alt-Ergo: The SMT Solver For Software Verification                     *)
+(*     Copyright (C) 2013-2018 --- OCamlPro SAS                               *)
+(*                                                                            *)
+(*     This file is distributed under the terms of the Apache Software        *)
+(*     License version 2.0                                                    *)
+(*                                                                            *)
+(******************************************************************************)
+ 
+(** Convert RGB color given in the decimal format (red, green, blue) where
+    red, green and blue are integers between 0 and 65535
+    to RGB color in hexadecimal format #rrrrggggbbbb where r, g, b are hexadecimal digits. *)
+val dec_to_hex_color : int -> int -> int -> string
diff --git a/src/bin/gui/main_gui.ml b/src/bin/gui/main_gui.ml
index 56e7b96e9..2f3f4fe29 100644
--- a/src/bin/gui/main_gui.ml
+++ b/src/bin/gui/main_gui.ml
@@ -194,12 +194,11 @@ let show_about () =
 let pop_error ?(error=false) ~message () =
   let pop_w = GWindow.dialog
       ~title:(if error then "Error" else "Warning")
-      ~allow_grow:true
       ~position:`CENTER
       ~width:400 ()
   in
   let bbox = GPack.button_box `HORIZONTAL ~border_width:5 ~layout:`END
-      ~child_height:20 ~child_width:85 ~spacing:10
+               (*~child_height:20 ~child_width:85*) ~spacing:10
       ~packing:pop_w#action_area#add () in
 
   let button_ok = GButton.button ~packing:bbox#add () in
@@ -220,7 +219,6 @@ let pop_error ?(error=false) ~message () =
 let pop_model sat_env () =
   let pop_w = GWindow.dialog
       ~title:"Model"
-      ~allow_grow:true
       ~destroy_with_parent:true
       ~position:`CENTER
       ~width:400
@@ -231,10 +229,10 @@ let pop_model sat_env () =
       ~vpolicy:`AUTOMATIC
       ~hpolicy:`AUTOMATIC
       ~packing:pop_w#vbox#add () in
-  let buf1 = GSourceView2.source_buffer () in
-  let tv1 = GSourceView2.source_view ~source_buffer:buf1 ~packing:(sw1#add)
-      ~wrap_mode:`CHAR () in
-  let _ = tv1#misc#modify_font monospace_font in
+  let buf1 = GSourceView3.source_buffer () in
+  let tv1 = GSourceView3.source_view ~source_buffer:buf1 ~packing:(sw1#add)
+              ~wrap_mode:`CHAR () in
+  let _ = tv1#misc#modify_font font in
   let _ = tv1#set_editable false in
   let model_text = asprintf "%a@." (SAT.print_model ~header:false) sat_env in
   buf1#set_text model_text;
@@ -778,7 +776,7 @@ let empty_error_model () =
 
 
 let goto_error (view:GTree.view) error_model buffer
-    (sv:GSourceView2.source_view)  path _column =
+    (sv:GSourceView3.source_view)  path _column =
   let model = view#model in
   let row = model#get_iter path in
   let line = model#get ~row ~column:error_model.rcol_line in
@@ -815,10 +813,8 @@ let create_error_view error_model buffer sv ~packing () =
            ~callback:(goto_error view error_model buffer sv));
   view
 
-
-
 let goto_lemma (view:GTree.view) inst_model buffer
-    (sv:GSourceView2.source_view) env path _column =
+    (sv:GSourceView3.source_view) env path _column =
   let model = view#model in
   let row = model#get_iter path in
   let id = model#get ~row ~column:inst_model.icol_tag in
@@ -834,9 +830,6 @@ let goto_lemma (view:GTree.view) inst_model buffer
     env.last_tag <- t;
   with Not_found -> ()
 
-
-let colormap () = Gdk.Color.get_system_colormap ()
-
 let set_color_inst inst_model renderer (istore:GTree.model) row =
   let id = istore#get ~row ~column:inst_model.icol_tag in
   let _, nb_inst, _, limit = Hashtbl.find inst_model.h id in
@@ -848,8 +841,7 @@ let set_color_inst inst_model renderer (istore:GTree.model) row =
     renderer#set_properties [`FOREGROUND "blue"]
   else if inst_model.max <> 0 then
     let perc = (nb_inst * 65535) / inst_model.max in
-    let red_n =
-      Gdk.Color.alloc ~colormap:(colormap ()) (`RGB (perc, 0, 0)) in
+    let red_n = Gdk.Color.color_parse (Gui_util.dec_to_hex_color perc 0 0) in
     renderer#set_properties [`FOREGROUND_GDK red_n]
   else
     renderer#set_properties [`FOREGROUND_SET false];
@@ -937,7 +929,7 @@ let prev_ends i buf found_all_tag =
   if !iter#compare buf#start_iter <= 0 then raise Not_found;
   !iter
 
-let search_next ?(backward=false) (sv:GSourceView2.source_view)
+let search_next ?(backward=false) (sv:GSourceView3.source_view)
     (buf:sbuffer) found_tag found_all_tag () =
   try
     let iter = buf#get_iter_at_char buf#cursor_position in
@@ -956,17 +948,15 @@ let search_next ?(backward=false) (sv:GSourceView2.source_view)
     buf#place_cursor ~where:i2
   with Not_found -> ()
 
-let search_one buf str result iter found_all_tag =
-  result :=
-    GSourceView2.iter_forward_search !iter []
-      ~start:buf#start_iter ~stop:buf#end_iter str;
+let search_one buf str result (iter:GText.iter ref) found_all_tag =
+  result := !iter#forward_search str;
   match !result with
   | None -> ()
-  | Some (i1, i2) ->
+  | Some (i1, i2) -> 
     buf#apply_tag found_all_tag ~start:i1 ~stop:i2;
     iter := i2
 
-let search_all entry (_sv:GSourceView2.source_view)
+let search_all entry (_sv:GSourceView3.source_view)
     (buf:sbuffer) found_tag found_all_tag () =
   buf#remove_tag found_tag ~start:buf#start_iter ~stop:buf#end_iter;
   buf#remove_tag found_all_tag ~start:buf#start_iter ~stop:buf#end_iter;
@@ -979,22 +969,18 @@ let search_all entry (_sv:GSourceView2.source_view)
       search_one buf str result iter found_all_tag
     done
 
-
 let start_gui all_used_context =
   Options.set_timers true;
   Options.set_thread_yield Thread.yield;
 
   (* TODO: crash : change this*)
   set_timeout (fun () ->
-      Printer.print_std "Timeout";
+      Printer.print_std "Timeout TODO";
       raise Util.Timeout);
 
-
   let w =
     GWindow.window
       ~title:"AltGr-Ergo"
-      ~allow_grow:true
-      ~allow_shrink:true
       ~position:`CENTER
       ~width:window_width
       ~height:window_height ()
@@ -1003,14 +989,14 @@ let start_gui all_used_context =
   ignore (w#misc#connect#size_allocate ~callback:(fun r ->
       Gui_config.update_window_size r.Gtk.width r.Gtk.height));
 
-  let lmanager = GSourceView2.source_language_manager ~default:true in
+  let lmanager = GSourceView3.source_language_manager ~default:true in
   lmanager#set_search_path
     (String.concat Filename.dir_sep
        [Config.datadir; "gtksourceview-2.0"; "language-specs"] ::
      lmanager#search_path);
   let source_language = lmanager#language "alt-ergo" in
 
-  let smanager = GSourceView2.source_style_scheme_manager ~default:true in
+  let smanager = GSourceView3.source_style_scheme_manager ~default:true in
   let scheme = smanager#style_scheme Gui_config.style in
   let filename = get_file () in
   let preludes = Options.get_preludes () in
@@ -1049,15 +1035,15 @@ let start_gui all_used_context =
          in
          let buf1 = match source_language with
            | Some language ->
-             GSourceView2.source_buffer ~language
+             GSourceView3.source_buffer ~language
                ~highlight_syntax:true ~highlight_matching_brackets:true ()
-           | None -> GSourceView2.source_buffer () in
+           | None -> GSourceView3.source_buffer () in
 
          let buf2 = match source_language with
            | Some language ->
-             GSourceView2.source_buffer ~language
+             GSourceView3.source_buffer ~language
                ~highlight_syntax:true ~highlight_matching_brackets:true ()
-           | None -> GSourceView2.source_buffer () in
+           | None -> GSourceView3.source_buffer () in
 
          buf1#set_style_scheme scheme;
          buf2#set_style_scheme scheme;
@@ -1097,7 +1083,8 @@ let start_gui all_used_context =
 
          let toolbox = GPack.hbox ~border_width:0 ~packing:rbox#pack () in
 
-         let toolbar = GButton.toolbar ~tooltips:true ~packing:toolbox#add () in
+         let toolbar = GButton.toolbar (*~tooltips:true*)
+                         ~packing:toolbox#add ~style: `BOTH () in
          toolbar#set_icon_size `DIALOG;
 
          let hb = GPack.paned `HORIZONTAL
@@ -1134,8 +1121,7 @@ let start_gui all_used_context =
              ~row_spacings:1 ~col_spacings:8 ~border_width:4
              ~packing:fr5#add () in
 
-
-         let st = GMisc.statusbar ~has_resize_grip:false ~border_width:0
+         let st = GMisc.statusbar ~border_width:0
              ~packing:vbox#pack () in
          let st_ctx = st#new_context ~name:"Type" in
 
@@ -1153,11 +1139,11 @@ let start_gui all_used_context =
              ~packing:fr1#add ()
          in
          let tv1 =
-           GSourceView2.source_view ~source_buffer:buf1 ~packing:(sw1#add)
+           GSourceView3.source_view ~source_buffer:buf1 ~packing:(sw1#add)
              ~show_line_numbers:true ~wrap_mode:(if wrap then `CHAR else `NONE)
              ~highlight_current_line:true ()
          in
-         let _ = tv1#misc#modify_font monospace_font in
+         let _ = tv1#misc#modify_font font in
          let _ = tv1#set_editable false in
 
          let sw2 = GBin.scrolled_window
@@ -1166,11 +1152,11 @@ let start_gui all_used_context =
              ~packing:fr2#add ()
          in
          let tv2 =
-           GSourceView2.source_view ~source_buffer:buf2 ~packing:(sw2#add)
+           GSourceView3.source_view ~source_buffer:buf2 ~packing:(sw2#add)
              ~show_line_numbers:false ~wrap_mode:(if wrap then `CHAR else `NONE)
              ~highlight_current_line:true ()
          in
-         let _ = tv2#misc#modify_font monospace_font in
+         let _ = tv2#misc#modify_font font in
          let _ = tv2#set_editable false in
 
 
@@ -1178,60 +1164,47 @@ let start_gui all_used_context =
              st_ctx annoted_ast dep actions resulting_ids in
          connect env;
 
-         ignore (toolbar#insert_toggle_button
-                   ~text:" Remove context"
-                   ~icon:(GMisc.image ~stock:`CUT
-                            ~icon_size:`LARGE_TOOLBAR ())#coerce
-                   ~callback:(remove_context env) ());
-
-         let buttonrun = toolbar#insert_button
-             ~text:" Run Alt-Ergo"
-             ~icon:(GMisc.image ~stock:`EXECUTE  ~icon_size:`LARGE_TOOLBAR()
-                   )#coerce () in
+         let remove_ctx_button = GButton.toggle_tool_button ~label:" Remove context"
+                                   ~stock:`CUT ~packing:toolbar#insert () in
+         ignore(remove_ctx_button#connect#clicked ~callback:(remove_context env));
+     
+         let run_button = GButton.tool_button ~label:" Run Alt-Ergo"
+                            ~stock:`EXECUTE () in 
+         toolbar#insert run_button;
 
-         let buttonstop = toolbar#insert_button
-             ~text:" Abort"
-             ~icon:(GMisc.image ~stock:`STOP  ~icon_size:`LARGE_TOOLBAR()
-                   )#coerce () in
-         buttonstop#misc#hide ();
+         let stop_button = GButton.tool_button ~label:" Abort" ~stock:`STOP () in 
+         stop_button#misc#hide ();
 
-         toolbar#insert_space ();
+         (* TODO: Use toolbar#insert instead of insert_space *)
+         (*toolbar#insert_space ();*)
 
-         let resultbox = GPack.hbox () in
+         let tool_item = GButton.tool_item () in
+         let result_box = GPack.hbox ~packing:tool_item#add () in
          let result_image = GMisc.image ~icon_size:`LARGE_TOOLBAR
-             ~stock:`DIALOG_QUESTION ~packing:resultbox#add () in
+             ~stock:`DIALOG_QUESTION ~packing:result_box#add () in
          let result_label = GMisc.label
-             ~text:" " ~packing:resultbox#add () in
+             ~text:" " ~packing:result_box#add () in
 
-         ignore(toolbar#insert_widget resultbox#coerce);
+         ignore(toolbar#insert tool_item);
 
-         let buttonclean = toolbar#insert_button
-             ~text:" Clean unused"
-             ~icon:(GMisc.image ~stock:`CLEAR  ~icon_size:`LARGE_TOOLBAR()
-                   )#coerce () in
-         buttonclean#misc#hide ();
+         let clean_button = GButton.tool_button ~label:" Clean unused" ~stock:`CLEAR () in
+         toolbar#insert clean_button;
+         clean_button#misc#hide ();
 
          let toolsearch =
-           GButton.toolbar ~tooltips:true ~packing:(toolbox#pack ~fill:true) ()
+           GButton.toolbar (*~tooltips:true*) ~packing:(toolbox#pack ~fill:true) ()
          in
          toolsearch#set_icon_size `DIALOG;
 
-         let search_box = GPack.hbox ~spacing:5 ~border_width:5 () in
+         let tool_item = GButton.tool_item ~packing:toolsearch#insert () in
+         let search_box = GPack.hbox ~spacing:5 ~border_width:5 ~packing:tool_item#add () in
          ignore(GMisc.image ~icon_size:`LARGE_TOOLBAR
                   ~stock:`FIND ~packing:search_box#add ());
          let search_entry = GEdit.entry ~packing:search_box#add () in
 
-         ignore(toolsearch#insert_widget search_box#coerce);
-
-         let button_seach_forw = toolsearch#insert_button
-             (* ~text:"Search" *)
-             ~icon:(GMisc.image ~stock:`GO_DOWN  ~icon_size:`LARGE_TOOLBAR()
-                   )#coerce () in
-         let button_seach_back = toolsearch#insert_button
-             (* ~text:"Search" *)
-             ~icon:(GMisc.image ~stock:`GO_UP  ~icon_size:`LARGE_TOOLBAR()
-                   )#coerce () in
-
+         let search_forw_button = GButton.tool_button ~stock:`GO_DOWN ~packing:toolsearch#insert () in
+         let search_back_button = GButton.tool_button ~stock:`GO_UP ~packing:toolsearch#insert () in
+       
          let found_all_tag = buf1#create_tag [`BACKGROUND "yellow"] in
          let found_tag = buf1#create_tag [`BACKGROUND "orange"] in
 
@@ -1248,14 +1221,12 @@ let start_gui all_used_context =
                       else false
                     ));
 
-         ignore(button_seach_forw#connect#clicked
+         ignore(search_forw_button#connect#clicked
                   ~callback:(search_next tv1 buf1 found_tag found_all_tag));
-         ignore(button_seach_back#connect#clicked
+         ignore(search_back_button#connect#clicked
                   ~callback:(search_next ~backward:true
                                tv1 buf1 found_tag found_all_tag));
 
-
-
          let sw3 = GBin.scrolled_window
              ~vpolicy:`AUTOMATIC
              ~hpolicy:`AUTOMATIC
@@ -1284,12 +1255,12 @@ let start_gui all_used_context =
 
          let thread = ref None in
 
-         ignore(buttonrun#connect#clicked
+         ignore(run_button#connect#clicked
                   ~callback:(
-                    run buttonrun buttonstop buttonclean inst_model timers_model
+                    run run_button stop_button clean_button inst_model timers_model
                       result_image result_label thread env used_context));
 
-         ignore(buttonstop#connect#clicked
+         ignore(stop_button#connect#clicked
                   ~callback:(kill_thread thread));
 
          ignore(eventBox#event#connect#key_press
@@ -1300,7 +1271,7 @@ let start_gui all_used_context =
 
          Hashtbl.add note_search !nb_page
            (search_entry,
-            run buttonrun buttonstop buttonclean inst_model
+            run run_button stop_button clean_button inst_model
               timers_model result_image result_label thread env used_context);
 
          env::acc
@@ -1317,7 +1288,7 @@ let start_gui all_used_context =
 
   let file_entries = [
     `I ("Save session", save_dialog "Cancel" envs);
-    `S;
+    (*`S;*)
     `I ("Quit", quit envs)
   ] in
 
@@ -1339,8 +1310,8 @@ let start_gui all_used_context =
         )) envs
   in
 
-
-  let choose_font () =
+  (* The GtkFontChooserDialog is not yet implemented by lablgtk3. *)           
+  (*let choose_font () =
     let font_win = GWindow.font_selection_dialog
         ~parent:w
         ~destroy_with_parent:true
@@ -1352,24 +1323,24 @@ let start_gui all_used_context =
     );
     ignore (font_win#run ());
     ignore (font_win#misc#hide ())
-  in
+    in*)
 
 
   let debug_entries = [
     `C ("SAT", get_debug_sat (), set_debug_sat);
-    `S;
+    (*`S;*)
     `C ("CC", get_debug_cc (), set_debug_cc);
     `C ("Use", get_debug_use (), set_debug_use);
     `C ("UF", get_debug_uf (), set_debug_uf);
     `C ("AC", get_debug_ac (), set_debug_ac);
-    `S;
+    (*`S;*)
     `C ("Arith", get_debug_arith (), set_debug_arith);
     `C ("Fourier-Motzkin", get_debug_fm (), set_debug_fm);
     `C ("Arrays", get_debug_arrays (), set_debug_arrays);
     `C ("Bit-vectors", get_debug_bitv (), set_debug_bitv);
     `C ("Sum", get_debug_sum (), set_debug_sum);
     `C ("Records", false, not_implemented);
-    `S;
+    (*`S;*)
     `C ("Case split", get_debug_split (), set_debug_split);
     `C ("Replay unsat cores", get_debug_unsat_core (), set_debug_unsat_core);
     `C ("Typing", get_debug_typing (), set_debug_typing);
@@ -1388,21 +1359,21 @@ let start_gui all_used_context =
       else set_instantiation_heuristic INormal in
     [
       `C ("Unsat cores", get_unsat_core (), set_unsat_core);
-      `S;
+      (*`S;*)
       `C ("Model", get_model (), set_model);
       `C ("Complete model", get_complete_model (), set_complete_model);
       `C ("All models", get_all_models (), set_all_models);
-      `S;
+      (*`S;*)
       `C ("Variables in triggers", get_triggers_var (), set_triggers_var);
       `C ("Greedy", get_greedy (), set_greedy);
       `C ("Contra congruence", not (get_no_contracongru ()),
           fun b -> set_no_contracongru (not b));
-      `S;
+      (*`S;*)
       `C ("Restricted", get_restricted (), set_restricted);
-      `S;
+      (*`S;*)
       `C ("Wrap lines", wrap, set_wrap_lines);
-      `S;
-      `I ("Change font", choose_font);
+      (*`S;*)
+      (*`I ("Change font", choose_font);*)
       `I ("Increase font size", fun () -> increase_size envs);
       `I ("Decrease font size", fun () -> decrease_size envs);
       `I ("Reset font size", fun () -> reset_size envs);
@@ -1418,7 +1389,7 @@ let start_gui all_used_context =
   (*   `M ("Options", options_entries); *)
   (*   `M ("Help", help_entries) *)
   (* ] in *)
-
+ 
   let create_menu label menubar =
     let item = GMenu.menu_item ~label ~packing:menubar#append () in
     GMenu.menu ~packing:item#set_submenu ()
@@ -1494,7 +1465,7 @@ let start_replay session_cin all_used_context =
     (fun (l, goal_name) ->
        let used_context = FE.choose_used_context all_used_context ~goal_name in
 
-       let buf1 = GSourceView2.source_buffer () in
+       let buf1 = GSourceView3.source_buffer () in
 
        let annoted_ast = annot buf1 l in
 
@@ -1522,7 +1493,6 @@ let start_replay session_cin all_used_context =
     | None -> ()
   end
 
-
 let () =
   Gui_config.init ();
   init_gtk ();

From af6b572a5d5ec41ec07c847ffea50eeedfeef0e5 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <tiky.halbaroth@gmail.com>
Date: Fri, 8 Jul 2022 15:32:19 +0200
Subject: [PATCH 2/6] Add lablgtk3-sourceview3 as a dependency of AltGr-Ergo

---
 altgr-ergo.opam | 1 +
 1 file changed, 1 insertion(+)

diff --git a/altgr-ergo.opam b/altgr-ergo.opam
index f96f57164..f6e0353c5 100644
--- a/altgr-ergo.opam
+++ b/altgr-ergo.opam
@@ -20,6 +20,7 @@ depends: [
   "alt-ergo-parsers" {= version}
   "lablgtk3"
   "conf-gtksourceview3"
+  "lablgtk3-sourceview3"
   "cmdliner" {>= "1.1.0"}
   "odoc" {with-doc}
 ]

From d5dd9a60bb66fe2e8bf9d3e60aabad12cf9682eb Mon Sep 17 00:00:00 2001
From: Pierre Villemot <tiky.halbaroth@gmail.com>
Date: Fri, 8 Jul 2022 16:46:55 +0200
Subject: [PATCH 3/6] Add the lablgtk3-sourceview3 dependency in dune-project
 since the opam files are generated by Dune.

---
 altgr-ergo.opam | 1 +
 dune-project    | 1 +
 2 files changed, 2 insertions(+)

diff --git a/altgr-ergo.opam b/altgr-ergo.opam
index f96f57164..f6e0353c5 100644
--- a/altgr-ergo.opam
+++ b/altgr-ergo.opam
@@ -20,6 +20,7 @@ depends: [
   "alt-ergo-parsers" {= version}
   "lablgtk3"
   "conf-gtksourceview3"
+  "lablgtk3-sourceview3"
   "cmdliner" {>= "1.1.0"}
   "odoc" {with-doc}
 ]
diff --git a/dune-project b/dune-project
index 6e01731fe..b97ad3a67 100644
--- a/dune-project
+++ b/dune-project
@@ -56,6 +56,7 @@ See more details on https://alt-ergo.ocamlpro.com/"
   (alt-ergo-parsers (= :version))
   lablgtk3
   conf-gtksourceview3
+  lablgtk3-sourceview3
   (cmdliner (>= 1.1.0))
   (odoc :with-doc)
 )

From 058a851401e908d1c10035b226f73af77dc20dac Mon Sep 17 00:00:00 2001
From: Pierre Villemot <tiky.halbaroth@gmail.com>
Date: Mon, 11 Jul 2022 11:38:03 +0200
Subject: [PATCH 4/6] Fix indentation

---
 src/bin/gui/connected_ast.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/bin/gui/connected_ast.ml b/src/bin/gui/connected_ast.ml
index 29feed4af..0979c2bc8 100644
--- a/src/bin/gui/connected_ast.ml
+++ b/src/bin/gui/connected_ast.ml
@@ -603,8 +603,8 @@ and popup_axiom t env _offset () =
       (* ~icon:(GdkPixbuf.from_xpm_data Logo.xpm_logo) ()  *)
   in
   let bbox = GPack.button_box `HORIZONTAL ~border_width:5 ~layout:`END
-               ~spacing:10
-      ~packing:pop_w#action_area#add () in
+      ~spacing:10 ~packing:pop_w#action_area#add ()
+  in
 
   let button_ok = GButton.button ~packing:bbox#add () in
   let phbox = GPack.hbox ~packing:button_ok#add () in
@@ -758,8 +758,8 @@ and popup_trigger t qid env (sbuf:sbuffer) offset () =
       (* ~icon:(GdkPixbuf.from_xpm_data Logo.xpm_logo) ()  *)
   in
   let bbox = GPack.button_box `HORIZONTAL ~border_width:5 ~layout:`END
-               ~spacing:10
-      ~packing:pop_w#action_area#add () in
+      ~spacing:10 ~packing:pop_w#action_area#add ()
+  in
 
   let button_ok = GButton.button ~packing:bbox#add () in
   let phbox = GPack.hbox ~packing:button_ok#add () in
@@ -781,9 +781,11 @@ and popup_trigger t qid env (sbuf:sbuffer) offset () =
   let sw1 = GBin.scrolled_window
       ~vpolicy:`AUTOMATIC
       ~hpolicy:`AUTOMATIC
-      ~packing:pop_w#vbox#add () in
+      ~packing:pop_w#vbox#add ()
+  in
   let tv1 = GSourceView3.source_view ~source_buffer:buf1 ~packing:(sw1#add)
-              ~show_line_numbers:true ~wrap_mode:`CHAR() in
+       ~show_line_numbers:true ~wrap_mode:`CHAR()
+  in
   let _ = tv1#misc#modify_font font in
   let _ = tv1#set_editable true in
 

From 12a561992c208a6371597c2f91ee6d3a51f5fe95 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <tiky.halbaroth@gmail.com>
Date: Mon, 11 Jul 2022 11:44:57 +0200
Subject: [PATCH 5/6] Improve readability

---
 src/bin/gui/annoted_ast.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/bin/gui/annoted_ast.ml b/src/bin/gui/annoted_ast.ml
index 709cb9a75..345dd0be5 100644
--- a/src/bin/gui/annoted_ast.ml
+++ b/src/bin/gui/annoted_ast.ml
@@ -35,7 +35,8 @@ open Options
 open Gui_config
 open Gui_session
 
-let font = GPango.font_description_from_string (font_family ^ " " ^ (string_of_int font_size))
+let font_str = Format.sprintf "%s %i" font_family font_size
+let font = GPango.font_description_from_string font_str
 let font_size = font#size
 
 let make_indent nb =

From 0671f150fe0b665a5e5ed7d044807c9202db8c24 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <tiky.halbaroth@gmail.com>
Date: Mon, 11 Jul 2022 11:49:39 +0200
Subject: [PATCH 6/6] Fix indentation and remove a TODO

---
 src/bin/gui/main_gui.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/bin/gui/main_gui.ml b/src/bin/gui/main_gui.ml
index 2f3f4fe29..df528f87c 100644
--- a/src/bin/gui/main_gui.ml
+++ b/src/bin/gui/main_gui.ml
@@ -198,8 +198,9 @@ let pop_error ?(error=false) ~message () =
       ~width:400 ()
   in
   let bbox = GPack.button_box `HORIZONTAL ~border_width:5 ~layout:`END
-               (*~child_height:20 ~child_width:85*) ~spacing:10
-      ~packing:pop_w#action_area#add () in
+      (*~child_height:20 ~child_width:85*) ~spacing:10
+      ~packing:pop_w#action_area#add ()
+  in
 
   let button_ok = GButton.button ~packing:bbox#add () in
   let phbox = GPack.hbox ~packing:button_ok#add () in
@@ -975,7 +976,7 @@ let start_gui all_used_context =
 
   (* TODO: crash : change this*)
   set_timeout (fun () ->
-      Printer.print_std "Timeout TODO";
+      Printer.print_std "Timeout";
       raise Util.Timeout);
 
   let w =