X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=6bf9e5e026ed6dc97a101c9ecde6a219e624c12c;hb=0dc8115859d7f482793315493adc0b619236e06c;hp=13668a8aecc318d7df036bf406467826e8bb639a;hpb=d7b5af5d8c6297f191cb644034b5b4cb7dfe86c1;p=helm.git

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 13668a8ae..6bf9e5e02 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -256,8 +256,7 @@ let similarsymbols_tag = `NAME similarsymbols_tag_name in
 let initial_statuses current baseuri =
  let status = new MatitaEngine.status baseuri in
  (match current with
-     Some current ->
-      NCicLibrary.time_travel status;
+     Some current -> NCicLibrary.time_travel status;
 (*
       (* MATITA 1.0: there is a known bug in invalidation; temporary fix here *)
       NCicEnvironment.invalidate () *)
@@ -789,6 +788,7 @@ object (self)
     List.iter (fun o -> o status) observers
 
   method activate =
+    NCicLibrary.replace self#status;
     self#notify
 
   method loadFromFile f =
@@ -829,12 +829,12 @@ object (self)
   method private _saveToBackupFile () =
     if buffer#modified then
       begin
-        let f = self#filename in
+        let f = self#filename ^ "~" in
         let oc = open_out f in
         output_string oc (buffer#get_text ~start:buffer#start_iter
                             ~stop:buffer#end_iter ());
         close_out oc;
-        HLog.debug ("backup " ^ f ^ " saved")                    
+        HLog.debug ("backup " ^ f ^ " saved")
       end
   
   method private reset_buffer =