Commit 3bb1fa27 authored by MARCHE Claude's avatar MARCHE Claude

IDE: font size is now saved in config

parent 47bc4f57
......@@ -33,6 +33,7 @@ type t =
{ mutable window_width : int;
mutable window_height : int;
mutable tree_width : int;
mutable font_size : int;
mutable verbose : int;
mutable default_prover : string; (* "" means none *)
mutable default_editor : string;
......@@ -65,7 +66,7 @@ type ide = {
ide_window_width : int;
ide_window_height : int;
ide_tree_width : int;
ide_task_height : int;
ide_font_size : int;
ide_verbose : int;
ide_intro_premises : bool;
ide_show_labels : bool;
......@@ -87,7 +88,7 @@ let default_ide =
{ ide_window_width = 1024;
ide_window_height = 768;
ide_tree_width = 512;
ide_task_height = 384;
ide_font_size = 10;
ide_verbose = 0;
ide_intro_premises = true;
ide_show_labels = false;
......@@ -114,8 +115,8 @@ let load_ide section =
get_int section ~default:default_ide.ide_window_height "window_height";
ide_tree_width =
get_int section ~default:default_ide.ide_tree_width "tree_width";
ide_task_height =
get_int section ~default:default_ide.ide_task_height "task_height";
ide_font_size =
get_int section ~default:default_ide.ide_font_size "font_size";
ide_verbose =
get_int section ~default:default_ide.ide_verbose "verbose";
ide_intro_premises =
......@@ -176,6 +177,7 @@ let load_config config original_config env =
{ window_height = ide.ide_window_height;
window_width = ide.ide_window_width;
tree_width = ide.ide_tree_width;
font_size = ide.ide_font_size;
verbose = ide.ide_verbose;
intro_premises= ide.ide_intro_premises ;
show_labels = ide.ide_show_labels ;
......@@ -217,6 +219,7 @@ let save_config t =
let ide = set_int ide "window_height" t.window_height in
let ide = set_int ide "window_width" t.window_width in
let ide = set_int ide "tree_width" t.tree_width in
let ide = set_int ide "font_size" t.font_size in
let ide = set_int ide "verbose" t.verbose in
let ide = set_bool ide "intro_premises" t.intro_premises in
let ide = set_bool ide "print_labels" t.show_labels in
......@@ -248,6 +251,11 @@ let save_config () = save_config (config ())
let get_main () = (get_main (config ()).config)
let incr_font_size n =
let c = config () in
let s = max (c.font_size + n) 4 in
c.font_size <- s;
s
(*
......
......@@ -15,6 +15,7 @@ type t =
{ mutable window_width : int;
mutable window_height : int;
mutable tree_width : int;
mutable font_size : int;
mutable verbose : int;
mutable default_prover : string;
mutable default_editor : string;
......@@ -52,6 +53,10 @@ val config : unit -> t
val get_main : unit -> Whyconf.main
val incr_font_size : int -> int
(** [incr_font_size n] increments current font size by [n] (can be negative)
and returns the new size *)
(*****************)
(* images, icons *)
(*****************)
......
......@@ -359,7 +359,6 @@ let counterexample_page,counterexample_tab =
(fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
let _ = GPack.hbox ~packing:(source_tab#pack ~expand:false) ()
let (_ : GPack.box) =
GPack.hbox ~packing:(source_tab#pack ~expand:false ?from:None ?fill:None
?padding:None) ()
......@@ -418,7 +417,8 @@ let counterexample_view =
let modifiable_sans_font_views = ref [goals_view#misc]
let modifiable_mono_font_views =
ref [task_view#misc;edited_view#misc;output_view#misc]
ref [task_view#misc;edited_view#misc;output_view#misc;
counterexample_view#misc]
let () = task_view#source_buffer#set_language why_lang
let () = task_view#set_highlight_current_line true
......@@ -650,14 +650,14 @@ let update_tabs a =
(Pp.string_of (Pp.hov 2 print) m.S.metas_added)
| _ -> ""
in
let counterexample_text =
let counterexample_text =
match a with
| S.Proof_attempt a ->
begin
match a.S.proof_state with
| S.Done r ->
add_model "" r.Call_provers.pr_model
| _ -> ""
| _ -> ""
end
| _ -> ""
in
......@@ -1338,34 +1338,25 @@ let exit_function ~destroy () =
let sans_font_family = "Sans"
let mono_font_family = "Monospace"
let font_size = ref 10
let change_font () =
let change_font size =
(*
Tools.resize_images (!Colors.font_size * 2 - 4);
*)
let sff = sans_font_family ^ " " ^ string_of_int !font_size in
let mff = mono_font_family ^ " " ^ string_of_int !font_size in
let sff = sans_font_family ^ " " ^ string_of_int size in
let mff = mono_font_family ^ " " ^ string_of_int size in
let sf = Pango.Font.from_string sff in
let mf = Pango.Font.from_string mff in
List.iter (fun v -> v#modify_font sf) !modifiable_sans_font_views;
List.iter (fun v -> v#modify_font mf) !modifiable_mono_font_views
let enlarge_font () =
incr font_size;
change_font ();
(*
GConfig.save ()
*)
()
let size = Gconfig.incr_font_size 1 in
change_font size
let reduce_font () =
decr font_size;
change_font ();
(*
GConfig.save ()
*)
()
let size = Gconfig.incr_font_size (-1) in
change_font size
let view_menu = factory#add_submenu "_View"
let view_factory = new GMenu.factory view_menu ~accel_group
......@@ -1912,7 +1903,7 @@ let source_view =
*)
let () = modifiable_mono_font_views :=
source_view#misc :: !modifiable_mono_font_views
let () = change_font ()
let () = change_font (Gconfig.incr_font_size 0)
let () = source_view#source_buffer#set_language None
let () = source_view#set_highlight_current_line true
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment