When matita is started on a non-existent file, it avoids creating it

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 8dc0cf3135a56b0e4a85e0984d6ad9ef8cc799c3..108b36bfb3f8738ac008a02f65bf1e7207488ef6 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -596,7 +596,7 @@ class gui () =
                 script#reset (); 
                 script#assignFileName f;
                 source_view#source_buffer#begin_not_undoable_action ();
-                script#loadFromFile (); 
+                script#loadFromFile f; 
                 source_view#source_buffer#end_not_undoable_action ();
                 console#message ("'"^f^"' loaded.\n");
                 self#_enableSaveTo f
@@ -713,18 +713,15 @@ class gui () =
       let script = MatitaScript.instance () in
       script#reset (); 
       script#assignFileName file;
-      if not (Sys.file_exists file) then
-        begin
-          let oc = open_out file in
-          let template = MatitaMisc.input_file BuildTimeConf.script_template in 
-          output_string oc template;
-          close_out oc
-        end;
-      source_view#source_buffer#begin_not_undoable_action ();
-      script#loadFromFile ();
-      source_view#source_buffer#end_not_undoable_action ();
-      console#message ("'"^file^"' loaded.");
-      self#_enableSaveTo file
+      let content =
+       if Sys.file_exists file then file
+       else BuildTimeConf.script_template
+      in
+       source_view#source_buffer#begin_not_undoable_action ();
+       script#loadFromFile content;
+       source_view#source_buffer#end_not_undoable_action ();
+       console#message ("'"^file^"' loaded.");
+       self#_enableSaveTo file
       
     method setStar name b =
       let l = main#scriptLabel in