]> matita.cs.unibo.it Git - helm.git/commitdiff
bugfix: save "~" backup together with the non-~ version instead of in the current dir
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 15 Sep 2005 09:37:38 +0000 (09:37 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 15 Sep 2005 09:37:38 +0000 (09:37 +0000)
helm/matita/matitaScript.ml

index 8bd0d60d1f2df270cdfcb582778fcd2b564aef40..8ef5146ca8d72689f65646d67e40ab02748fe5b6 100644 (file)
@@ -449,17 +449,14 @@ object (self)
     
   method private ppFilename =
     match guistuff.filenamedata with 
-    | Some f,_ -> Filename.basename 
+    | Some f,_ -> f 
     | None,_ -> sprintf ".unnamed%d.ma" scriptId
   
   initializer 
-    ignore(GMain.Timeout.add ~ms:300000 
-       ~callback:(fun _ -> self#_saveToBackuptFile ();true));
-    ignore(buffer#connect#modified_changed 
-       (fun _ -> if buffer#modified then 
-          set_star self#ppFilename true 
-        else 
-          set_star self#ppFilename false))
+    ignore (GMain.Timeout.add ~ms:300000 
+       ~callback:(fun _ -> self#_saveToBackupFile ();true));
+    ignore (buffer#connect#modified_changed 
+      (fun _ -> set_star (Filename.basename self#ppFilename) buffer#modified))
 
   val mutable statements = [];    (** executed statements *)
   val mutable history = [ init ];
@@ -601,7 +598,7 @@ object (self)
     close_out oc;
     buffer#set_modified false
   
-  method private _saveToBackuptFile () =
+  method private _saveToBackupFile () =
     if buffer#modified then
       begin
         let f = self#ppFilename ^ "~" in
@@ -636,7 +633,7 @@ object (self)
     guistuff.filenamedata <- 
       (None,MatitamakeLib.development_for_dir (Unix.getcwd ()));
     buffer#set_modified false;
-    set_star self#ppFilename false
+    set_star (Filename.basename self#ppFilename) false
 
   method goto (pos: [`Top | `Bottom | `Cursor]) () =
     let old_locked_mark =