From e5a7ed72ab03f5fd0b32323de3923a69bd0a0031 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 15 Sep 2005 09:37:38 +0000 Subject: [PATCH] bugfix: save "~" backup together with the non-~ version instead of in the current dir --- helm/matita/matitaScript.ml | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) 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 = -- 2.39.2