fixed save/exit stuff

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 043fc31e43d45825f621dd485494645751b687f6..0d6bfedee5ea0ec6d6ef68a3e904ad6389be5580 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -298,7 +298,7 @@ object (self)
   val mutable filename = std_filename
   
   initializer 
-    ignore(GMain.Timeout.add ~ms:20000 
+    ignore(GMain.Timeout.add ~ms:30000 
        ~callback:(fun _ -> self#_saveToBackuptFile ();true));
     ignore(buffer#connect#modified_changed 
        (fun _ -> if buffer#modified then 
@@ -414,12 +414,15 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     buffer#set_modified false
   
   method private _saveToBackuptFile () =
-    let f = 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;
-    MatitaLog.debug ("backup file " ^ f ^ " saved")
+    if buffer#modified then
+      begin
+        let f = 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;
+        MatitaLog.debug ("backup " ^ f ^ " saved")                    
+      end
   
   method private goto_top =
     MatitaSync.time_travel ~present:self#status ~past:init;