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
let ask_and_save_moo_if_needed parent fname status =
let save () =
- MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev
- in
- if (MatitaScript.instance ())#eos then
+ MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev in
+ if (MatitaScript.instance ())#eos &&
+ status.MatitaTypes.proof_status = MatitaTypes.No_proof
+ then
begin
let mooname =
MatitaMisc.obj_file_of_script fname
let newScript () =
(s ())#reset ();
(s ())#template ();
- disableSave ()
+ disableSave ();
+ script_fname <- None
in
let cursor () =
source_buffer#place_cursor
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