Migrating lablgtk3

altgr-ergo.opam

@@ -18,8 +18,9 @@ depends: [
   "dune" {>= "2.0" & < "3.0"}
   "alt-ergo-lib" {= version}
   "alt-ergo-parsers" {= version}
-  "lablgtk"
-  "conf-gtksourceview"
+  "lablgtk3"
+  "conf-gtksourceview3"
+  "lablgtk3-sourceview3"
   "cmdliner" {>= "1.1.0"}
   "odoc" {with-doc}
 ]

dune-project

@@ -54,8 +54,9 @@ 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
+  lablgtk3-sourceview3
   (cmdliner (>= 1.1.0))
   (odoc :with-doc)
 )

src/bin/gui/annoted_ast.ml

@@ -35,14 +35,14 @@ 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_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 =
-  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 +203,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 +229,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 +342,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:"";

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

src/bin/gui/connected_ast.ml

@@ -598,14 +598,13 @@ 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
-      ~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
@@ -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,14 +753,13 @@ 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
-      ~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
@@ -772,20 +771,22 @@ 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
+      ~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
+  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 +820,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 +967,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
 
 

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

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,18 +85,21 @@ 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
 
 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