X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=f3b531fb285dee2bc6e60e46044fe1e5177acc12;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=5a6377b3bb66d768d798a71abaea8386e6b30b3c;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 5a6377b3b..f3b531fb2 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -63,7 +63,8 @@ class gui () =
   object (self)
     val mutable chosen_file = None
     val mutable _ok_not_exists = false
-
+    val mutable script_fname = None 
+   
     initializer
         (* glade's check widgets *)
       List.iter (fun w -> w#check_widgets ())
@@ -144,7 +145,7 @@ 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));
+      connect_button tbar#autoButton (tac (A.Auto (loc,None)));
         (* quit *)
       self#setQuitCallback (fun () -> exit 0);
         (* log *)
@@ -155,33 +156,37 @@ class gui () =
              (sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
         (* script *)
       let s () = MatitaScript.instance () in
-      let script_fname = ref None in
-      let enable_save_to f =
-        script_fname := Some f;
-        self#main#saveMenuItem#misc#set_sensitive true
-      in
-      let disable_save () =
-        script_fname := None;
+      let disableSave () =
+        script_fname <- None;
         self#main#saveMenuItem#misc#set_sensitive false
       in
       let loadScript () =
         let script = s () in
         match self#chooseFile () with
-        | Some f -> script#reset (); script#loadFrom f; enable_save_to f
+        | Some f -> 
+              script#reset (); 
+              script#loadFrom f; 
+              console#message ("'"^f^"' loaded.");
+              self#_enableSaveTo f
         | None -> ()
       in
       let saveAsScript () =
         let script = s () in
         match self#chooseFile ~ok_not_exists:true () with
-        | Some f -> script#saveTo f; enable_save_to f
+        | Some f -> 
+              script#saveTo f; 
+              console#message ("'"^f^"' saved.");
+              self#_enableSaveTo f
         | None -> ()
       in
       let saveScript () =
-        match !script_fname with
+        match script_fname with
         | None -> saveAsScript ()
-        | Some f -> (s ())#saveTo f
+        | Some f -> 
+              (s ())#saveTo f;
+              console#message ("'"^f^"' saved.");
       in
-      let newScript () = (s ())#reset (); disable_save () in
+      let newScript () = (s ())#reset (); disableSave () in
       let cursor () =
         let buf = self#main#scriptTextView#buffer in
         buf#place_cursor (buf#get_iter_at_mark (`NAME "locked"))
@@ -228,6 +233,18 @@ class gui () =
       self#main#hintHighImage#set_file "icons/matita-bulb-high.png";
         (* focus *)
       self#main#scriptTextView#misc#grab_focus ()
+    
+    method loadScript file =       
+      let script = MatitaScript.instance () in
+      script#reset (); 
+      script#loadFrom file; 
+      console#message ("'"^file^"' loaded.");
+      self#_enableSaveTo file
+        
+    method private _enableSaveTo file =
+      script_fname <- Some file;
+      self#main#saveMenuItem#misc#set_sensitive true
+        
 
     method console = console
 
@@ -312,7 +329,8 @@ let is_var_uri s =
 
 let interactive_uri_choice
   ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
-  ?(msg = "") ?(nonvars_button = false) ()
+  ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false) 
+  ?(hide_try=false) ?(ok_label="_Auto") ?copy_cb ()
   ~id uris
 =
   let gui = instance () in
@@ -323,11 +341,28 @@ let interactive_uri_choice
     Lazy.force nonvars_uris
   else begin
     let dialog = gui#newUriDialog () in
+    if hide_uri_entry then
+      dialog#uriEntryHBox#misc#hide ();
+    if hide_try then
+      begin
+      dialog#uriChoiceSelectedButton#misc#hide ();
+      dialog#uriChoiceConstantsButton#misc#hide ();
+      end;
+    dialog#okLabel#set_label ok_label;  
     dialog#uriChoiceTreeView#selection#set_mode
       (selection_mode :> Gtk.Tags.selection_mode);
     let model = new stringListModel dialog#uriChoiceTreeView in
     let choices = ref None in
     let nonvars = ref false in
+    (match copy_cb with
+    | None -> ()
+    | Some cb ->
+        dialog#copyButton#misc#show ();
+        connect_button dialog#copyButton 
+        (fun _ ->
+          match model#easy_selection () with
+          | [u] -> (cb u)
+          | _ -> ()));
     dialog#uriChoiceDialog#set_title title;
     dialog#uriChoiceLabel#set_text msg;
     List.iter model#easy_append uris;