added decrease and increase font size fantafeature

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 66cc8b0ffc9ab06aec984c4e205e0ccf720da4ea..cdbfc799a054f28e1743e1e941507e240949d22e 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -77,11 +77,16 @@ class gui () =
       ~packing:main#scriptScrolledWin#add
       ()
   in
+  let default_font_size =
+    Helm_registry.get_opt_default Helm_registry.int
+      ~default:BuildTimeConf.default_font_size "matita.font_size"
+  in
   let source_buffer = source_view#source_buffer in
   object (self)
     val mutable chosen_file = None
     val mutable _ok_not_exists = false
-    val mutable script_fname = None 
+    val mutable script_fname = None
+    val mutable font_size = default_font_size
    
     initializer
         (* glade's check widgets *)
@@ -267,19 +272,7 @@ class gui () =
             "\n";
           advance ());
          (* script monospace font stuff *)  
-      let font =
-        Helm_registry.get_opt_default Helm_registry.string
-          ~default:BuildTimeConf.default_script_font "matita.script_font"
-      in
-(*       let monospace_tag = 
-        source_buffer#create_tag [`FONT_DESC font] 
-      in *)
-      self#sourceView#misc#modify_font_by_name font;
-(*       let _ = 
-        source_buffer#connect#changed ~callback:(fun _ ->
-          let start, stop = source_buffer#bounds in
-          source_buffer#apply_tag monospace_tag start stop)
-      in *)
+      self#updateFontSize ();
         (* debug menu *)
       self#main#debugMenu#misc#hide ();
         (* status bar *)
@@ -381,6 +374,22 @@ class gui () =
       GtkThread.main ();
       !text
 
+    method private updateFontSize () =
+      self#sourceView#misc#modify_font_by_name
+        (sprintf "%s %d" BuildTimeConf.script_font font_size)
+
+    method increaseFontSize () =
+      font_size <- font_size + 1;
+      self#updateFontSize ()
+
+    method decreaseFontSize () =
+      font_size <- font_size - 1;
+      self#updateFontSize ()
+
+    method resetFontSize () =
+      font_size <- default_font_size;
+      self#updateFontSize ()
+
   end
 
 let gui () =