X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=5ea3903835f05dafa4a83dc4c6b2711b84aa3a5d;hb=08791e80816548121e81e04d3ead8c9a5171d033;hp=8e16be52cdb5a45cf4df39527b1ef6ef421fb618;hpb=ccee7ed50388a3953ce3cae38b5c524b152d92b2;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 8e16be52c..5ea390383 100644 --- 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