version 0.7.1

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 8e16be52cdb5a45cf4df39527b1ef6ef421fb618..5ea3903835f05dafa4a83dc4c6b2711b84aa3a5d 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -42,7 +42,7 @@ end
 class console ~(buffer: GText.buffer) () =
   object (self)
     val error_tag   = buffer#create_tag [ `FOREGROUND "red" ]
-    val warning_tag = buffer#create_tag [ `FOREGROUND "yellow" ]
+    val warning_tag = buffer#create_tag [ `FOREGROUND "orange" ]
     val message_tag = buffer#create_tag []
     val debug_tag   = buffer#create_tag [ `FOREGROUND "#888888" ]
     method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s
@@ -389,7 +389,14 @@ class gui () =
       let script = MatitaScript.instance () in
       script#reset (); 
       script#assignFileName file;
-      script#loadFromFile (); 
+      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;
+      script#loadFromFile ();
       console#message ("'"^file^"' loaded.");
       self#_enableSaveTo file