diff --git a/altgr-ergo.opam b/altgr-ergo.opam index 496ae843b..f6e0353c5 100644 --- a/altgr-ergo.opam +++ b/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} ] diff --git a/dune-project b/dune-project index cc5d947c3..b97ad3a67 100644 --- a/dune-project +++ b/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) ) diff --git a/src/bin/gui/annoted_ast.ml b/src/bin/gui/annoted_ast.ml index 08fd7eec8..345dd0be5 100644 --- a/src/bin/gui/annoted_ast.ml +++ b/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:""; 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..0979c2bc8 100644 --- a/src/bin/gui/connected_ast.ml +++ b/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 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..df528f87c 100644 --- a/src/bin/gui/main_gui.ml +++ b/src/bin/gui/main_gui.ml @@ -194,13 +194,13 @@ 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 - ~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 @@ -220,7 +220,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 +230,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 +777,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 +814,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 +831,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 +842,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 +930,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 +949,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,7 +970,6 @@ 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; @@ -989,12 +979,9 @@ let start_gui all_used_context = Printer.print_std "Timeout"; 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 +990,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 +1036,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 +1084,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 +1122,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 +1140,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 +1153,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 +1165,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 +1222,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 +1256,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 +1272,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 +1289,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 +1311,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 +1324,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 +1360,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 +1390,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 +1466,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 +1494,6 @@ let start_replay session_cin all_used_context = | None -> () end - let () = Gui_config.init (); init_gtk ();