From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 15 Sep 2005 09:37:38 +0000 (+0000)
Subject: bugfix: save "~" backup together with the non-~ version instead of in the current dir
X-Git-Tag: LAST_BEFORE_NEW~126
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e5a7ed72ab03f5fd0b32323de3923a69bd0a0031;p=helm.git

bugfix: save "~" backup together with the non-~ version instead of in the current dir
---

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 8bd0d60d1..8ef5146ca 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -449,17 +449,14 @@ object (self)
     
   method private ppFilename =
     match guistuff.filenamedata with 
-    | Some f,_ -> Filename.basename f 
+    | 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 =