added autosave and * (modified feature)

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index e2b4d4682830a4950793421987a1048d370b9521..1e2b548267d9f95f31da8221b3c97c81fca90d0b 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -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;