increase/decrease font sizes

src/ide/gconfig.ml

@@ -270,12 +270,50 @@ let save_config () = save_config (config ())
 
 let get_main () = (get_main (config ()).config)
 
+(*
+
+
+  font size
+
+
+ *)
+
+
+let sans_font_family = "Sans"
+let mono_font_family = "Monospace"
+
+let modifiable_sans_font_views = ref []
+let modifiable_mono_font_views = ref []
+
+let add_modifiable_sans_font_view v =
+  modifiable_sans_font_views := v :: !modifiable_sans_font_views
+
+let add_modifiable_mono_font_view v =
+  modifiable_mono_font_views := v :: !modifiable_mono_font_views
+
+let change_font size =
+(*
+  Tools.resize_images (!Colors.font_size * 2 - 4);
+*)
+  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 incr_font_size n =
   let c = config () in
   let s = max (c.font_size + n) 4 in
   c.font_size <- s;
   s
 
+let enlarge_fonts () = change_font (incr_font_size 1)
+
+let reduce_fonts () = change_font (incr_font_size (-1))
+
+let set_fonts () = change_font (incr_font_size 0)
+
 (*
 
   images, icons
@@ -1199,6 +1237,8 @@ let uninstalled_prover c eS unknown =
     c.config <- set_prover_upgrade_policy c.config unknown policy;
     policy
 
+
+
 (*
 Local Variables:
 compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"

src/ide/gconfig.mli

@@ -56,9 +56,15 @@ 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 *)
+(*******************)
+(*   font size     *)
+(*******************)
+
+val add_modifiable_sans_font_view : GObj.misc_ops -> unit
+val add_modifiable_mono_font_view : GObj.misc_ops -> unit
+val enlarge_fonts : unit -> unit
+val reduce_fonts : unit -> unit
+val set_fonts : unit -> unit
 
 (*****************)
 (* images, icons *)

src/ide/gmain.ml

@@ -417,14 +417,14 @@ let counterexample_view =
     ~packing:scrolled_counterexample_view#add
     ()
 
-let modifiable_sans_font_views = ref [goals_view#misc]
-let modifiable_mono_font_views =
-  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
-
+let () =
+  Gconfig.add_modifiable_sans_font_view goals_view#misc;
+  Gconfig.add_modifiable_mono_font_view task_view#misc;
+  Gconfig.add_modifiable_mono_font_view edited_view#misc;
+  Gconfig.add_modifiable_mono_font_view output_view#misc;
+  Gconfig.add_modifiable_mono_font_view counterexample_view#misc;
+  task_view#source_buffer#set_language why_lang;
+  task_view#set_highlight_current_line true
 
 let clear model = model#clear ()
 
@@ -1365,28 +1365,6 @@ let exit_function ~destroy () =
 (* View menu *)
 (*************)
 
-let sans_font_family = "Sans"
-let mono_font_family = "Monospace"
-
-let change_font size =
-(*
-  Tools.resize_images (!Colors.font_size * 2 - 4);
-*)
-  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 () =
-  let size = Gconfig.incr_font_size 1 in
-  change_font size
-
-let reduce_font () =
-  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
 

src/ide/why3ide.ml

@@ -108,6 +108,8 @@ let factory = new GMenu.factory menubar
 
 let accel_group = factory#accel_group
 
+(* 1.1 "File" menu *)
+
 let file_menu = factory#add_submenu "_File"
 let file_factory = new GMenu.factory file_menu ~accel_group
 
@@ -128,6 +130,13 @@ let (_ : GMenu.menu_item) =
   file_factory#add_item ~key:GdkKeysyms._Q "_Quit"
     ~callback:(exit_function ~destroy:false)
 
+
+(* 1.2 "View" menu
+
+   the entries in that menu are defined later
+
+*)
+
 (* 2. horizontal box contains:
    2.1 TODO: a tool box ?
    2.2 a horizontal paned containing:
@@ -219,13 +228,15 @@ let hbox22221 =
   GPack.hbox
     ~packing:(vbox2222#pack ?from:None ?expand:None ?fill:None ?padding:None) ()
 
-let command_entry = GEdit.entry ~packing:hbox22221#add ()
-
 let monitor =
   GMisc.label
-    ~text:"0/0/0"
+    ~text:"  0/0/0"
+    ~width:80
+    ~xalign:0.0
     ~packing:(hbox22221#pack ?from:None ?expand:None ?fill:None ?padding:None) ()
 
+let command_entry = GEdit.entry ~packing:hbox22221#add ()
+
 let message_zone =
   let sv = GBin.scrolled_window
       ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
@@ -249,11 +260,45 @@ let update_monitor =
   fun t s r ->
   reset_gc ();
   incr c;
-  let r =
-    if r=0 then "0" else
-      (string_of_int r) ^ " " ^ (fan (!c / 4))
-  in
-  monitor#set_text ((string_of_int t) ^ "/" ^ (string_of_int s) ^ "/" ^ r)
+  let f = if r=0 then "  " else fan (!c / 2) ^ " " in
+  monitor#set_text
+    (f ^ (string_of_int t) ^ "/" ^ (string_of_int s) ^ "/" ^ (string_of_int r))
+
+
+(*******************************)
+(* commands of the "View" menu *)
+(*******************************)
+
+let view_menu = factory#add_submenu "_View"
+let view_factory = new GMenu.factory view_menu ~accel_group
+
+(* goals view is not yet multi-selectable
+let (_ : GMenu.image_menu_item) =
+  view_factory#add_image_item ~key:GdkKeysyms._A
+    ~label:"Select all"
+    ~callback:(fun () -> goals_view#selection#select_all ()) ()
+ *)
+
+let (_ : GMenu.menu_item) =
+  view_factory#add_item ~key:GdkKeysyms._plus
+    ~callback:enlarge_fonts "Enlarge font"
+
+let (_ : GMenu.menu_item) =
+    view_factory#add_item ~key:GdkKeysyms._minus
+      ~callback:reduce_fonts "Reduce font"
+
+let (_ : GMenu.image_menu_item) =
+  view_factory#add_image_item ~key:GdkKeysyms._E
+    ~label:"Expand all" ~callback:(fun () -> goals_view#expand_all ()) ()
+
+
+let () =
+  Gconfig.add_modifiable_sans_font_view goals_view#misc;
+  Gconfig.add_modifiable_mono_font_view monitor#misc;
+  Gconfig.add_modifiable_mono_font_view task_view#misc;
+  Gconfig.add_modifiable_mono_font_view command_entry#misc;
+  Gconfig.add_modifiable_mono_font_view message_zone#misc;
+  Gconfig.set_fonts ()
 
 (****************************)
 (* command entry completion *)
@@ -568,10 +613,12 @@ let on_selected_row r =
   let index = goals_model#get ~row:r#iter ~column:index_column in
   try
     let session_element = Hint.find model_index index in
+(*
     let () = match session_element with
              | IproofNode id -> Hpn.add pn_id_to_gtree id r (* TODO maybe not the good place to fill
                                                                     this table *)
              | _ -> () in
+ *)
     current_selected_index := session_element;
     match session_element with
     | IproofNode id ->