X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=34cf20afa4eb42bb0232ee13cd680e9faf024137;hb=e2fb8962f72096d3f0bb19f40b00a3502a11e932;hp=66cc8b0ffc9ab06aec984c4e205e0ccf720da4ea;hpb=98b94263fd97dc8d580e85ceabae30bf731d58e3;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 66cc8b0ff..34cf20afa 100644
--- 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 () = 
@@ -392,11 +401,6 @@ let instance = singleton gui
 
 let non p x = not (p x)
 
-let is_var_uri s =
-  try
-    String.sub s (String.length s - 4) 4 = ".var"
-  with Invalid_argument _ -> false
-
 (* this is a shit and should be changed :-{ *)
 let interactive_uri_choice
   ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
@@ -406,7 +410,7 @@ let interactive_uri_choice
   ~id uris
 =
   let gui = instance () in
-  let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in
+  let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in
   if (selection_mode <> `SINGLE) &&
     (Helm_registry.get_bool "matita.auto_disambiguation")
   then
@@ -437,7 +441,7 @@ let interactive_uri_choice
           | _ -> ()));
     dialog#uriChoiceDialog#set_title title;
     dialog#uriChoiceLabel#set_text msg;
-    List.iter model#easy_append uris;
+    List.iter model#easy_append (List.map UriManager.string_of_uri uris);
     dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
     let return v =
       choices := v;
@@ -455,11 +459,11 @@ let interactive_uri_choice
       connect_button dialog#uriChoiceAutoButton (fun _ ->
         match model#easy_selection () with
         | [] -> ()
-        | uris -> return (Some uris));
+        | uris -> return (Some (List.map UriManager.uri_of_string uris)));
     connect_button dialog#uriChoiceSelectedButton (fun _ ->
       match model#easy_selection () with
       | [] -> ()
-      | uris -> return (Some uris));
+      | uris -> return (Some (List.map UriManager.uri_of_string uris)));
     connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
     dialog#uriChoiceDialog#show ();
     GtkThread.main ();