X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=1e2b548267d9f95f31da8221b3c97c81fca90d0b;hb=ded3a0b12793fc8e463a4a3be9f62f54f734897e;hp=8eec3244d29915ff57768b0acb1f0de7961c2cc4;hpb=842919f2f8ee71a5301ad962220569450340a9e9;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 8eec3244d..1e2b54826 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -167,7 +167,7 @@ class gui () =
       connect_button tbar#transitivityButton
         (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#cutButton (tac_w_term (A.Cut (loc, None, hole)));
       connect_button tbar#autoButton (tac (A.Auto (loc,None,None)));
       MatitaGtkMisc.toggle_widget_visibility
        ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
@@ -211,7 +211,8 @@ class gui () =
         match self#chooseFile () with
         | Some f -> 
               script#reset (); 
-              script#loadFrom f; 
+              script#assignFileName f;
+              script#loadFromFile (); 
               console#message ("'"^f^"' loaded.\n");
               self#_enableSaveTo f
         | None -> ()
@@ -220,7 +221,8 @@ class gui () =
         let script = s () in
         match self#chooseFile ~ok_not_exists:true () with
         | Some f -> 
-              script#saveTo f; 
+              script#assignFileName f;
+              script#saveToFile (); 
               console#message ("'"^f^"' saved.\n");
               self#_enableSaveTo f
         | None -> ()
@@ -229,7 +231,8 @@ class gui () =
         match script_fname with
         | None -> saveAsScript ()
         | Some f -> 
-              (s ())#saveTo f;
+              (s ())#assignFileName f;
+              (s ())#saveToFile ();
               console#message ("'"^f^"' saved.\n");
       in
       let newScript () = (s ())#reset (); disableSave () in
@@ -293,9 +296,17 @@ class gui () =
     method loadScript file =       
       let script = MatitaScript.instance () in
       script#reset (); 
-      script#loadFrom file; 
+      script#assignFileName file;
+      script#loadFromFile (); 
       console#message ("'"^file^"' loaded.");
       self#_enableSaveTo file
+      
+    method setStar name b =
+      let l = main#scriptLabel in
+      if b then
+        l#set_text (name ^  " *")
+      else
+        l#set_text (name)
         
     method private _enableSaveTo file =
       script_fname <- Some file;