Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Migrating lablgtk3 #513

Merged
merged 7 commits into from
Jul 11, 2022
Merged

Migrating lablgtk3 #513

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
42a0c26
Migrate Alt-Ergo from lablgtk2 to lablgtk3.
Halbaroth Jun 30, 2022
af6b572
Add lablgtk3-sourceview3 as a dependency of AltGr-Ergo
Halbaroth Jul 8, 2022
d5dd9a6
Add the lablgtk3-sourceview3 dependency in dune-project since the opa…
Halbaroth Jul 8, 2022
8029c40
Merge branch 'migrating-lablgtk3' of github.com:Halbaroth/alt-ergo in…
Halbaroth Jul 8, 2022
058a851
Fix indentation
Halbaroth Jul 11, 2022
12a5619
Improve readability
Halbaroth Jul 11, 2022
0671f15
Fix indentation and remove a TODO
Halbaroth Jul 11, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions altgr-ergo.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,9 @@ depends: [
"dune" {>= "2.0" & < "3.0"}
"alt-ergo-lib" {= version}
"alt-ergo-parsers" {= version}
"lablgtk"
"conf-gtksourceview"
"lablgtk3"
"conf-gtksourceview3"
Copy link
Collaborator

@Stevendeo Stevendeo Jul 7, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Build failed on my side without lablgtk3-sourceview3, should it be an additional dependency?

"lablgtk3-sourceview3"
"cmdliner" {>= "1.1.0"}
"odoc" {with-doc}
]
Expand Down
5 changes: 3 additions & 2 deletions dune-project
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
)
Expand Down
81 changes: 29 additions & 52 deletions src/bin/gui/annoted_ast.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Halbaroth marked this conversation as resolved.
Show resolved Hide resolved
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;
Expand Down Expand Up @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -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:"";
Expand Down
16 changes: 7 additions & 9 deletions src/bin/gui/annoted_ast.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand All @@ -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 ->
Expand Down
45 changes: 22 additions & 23 deletions src/bin/gui/connected_ast.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Halbaroth marked this conversation as resolved.
Show resolved Hide resolved
~packing:pop_w#action_area#add () in

let button_ok = GButton.button ~packing:bbox#add () in
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Halbaroth marked this conversation as resolved.
Show resolved Hide resolved
~packing:pop_w#action_area#add () in

let button_ok = GButton.button ~packing:bbox#add () in
Expand All @@ -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
Halbaroth marked this conversation as resolved.
Show resolved Hide resolved
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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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


Expand Down
4 changes: 2 additions & 2 deletions src/bin/gui/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
)
Expand Down
27 changes: 15 additions & 12 deletions src/bin/gui/gui_config.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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 ] ->
Expand All @@ -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
Expand All @@ -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

Expand Down
9 changes: 6 additions & 3 deletions src/bin/gui/gui_config.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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

Expand Down
Loading