* the auto AST now has the width

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index c891a0bde63ec069fd9ec1207adde788589aa40a..8eec3244d29915ff57768b0acb1f0de7961c2cc4 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 *)
@@ -163,12 +168,14 @@ class gui () =
         (tac_w_term (A.Transitivity (loc, hole)));
       connect_button tbar#assumptionButton (tac (A.Assumption loc));
       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, hole)));
-      connect_button tbar#autoButton (tac (A.Auto (loc,None)));
+      connect_button tbar#autoButton (tac (A.Auto (loc,None,None)));
       MatitaGtkMisc.toggle_widget_visibility
        ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
        ~check:self#main#tacticsBarMenuItem;
       let module Hr = Helm_registry in
-      if not(Hr.get_opt_default Hr.get_bool false "matita.tactics_bar") then 
+      if
+        not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
+      then 
         self#main#tacticsBarMenuItem#set_active false;
       MatitaGtkMisc.toggle_callback 
         ~callback:(function 
@@ -265,19 +272,7 @@ class gui () =
             "\n";
           advance ());
          (* script monospace font stuff *)  
-      let font =
-        Helm_registry.get_opt_default Helm_registry.get
-          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 *)
@@ -379,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 () = 
@@ -390,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 = "")
@@ -404,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
@@ -435,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;
@@ -453,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 ();