match filename with Some f -> f | None -> sprintf ".unnamed%d.ma" scriptId
initializer
- ignore(GMain.Timeout.add ~ms:30000
+ ignore(GMain.Timeout.add ~ms:300000
~callback:(fun _ -> self#_saveToBackuptFile ();true));
- set_star self#ppFilename false;
ignore(buffer#connect#modified_changed
(fun _ -> if buffer#modified then
set_star self#ppFilename true
else
set_star self#ppFilename false));
self#reset ();
- self#template ();
- buffer#set_modified false
+ self#template ()
val mutable statements = []; (** executed statements *)
val mutable history = [ init ];
try
self#_advance ?statement ();
self#notify
- with Margin -> ()
+ with Margin -> self#notify
method retract () =
try
self#_retract ();
self#notify
- with Margin -> ()
+ with Margin -> self#notify
method private getFuture =
buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark))
method reset () =
self#goto_top;
buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter;
- self#notify
+ self#notify;
+ buffer#set_modified false
method template () =
let template = MatitaMisc.input_file BuildTimeConf.script_template in
- buffer#insert ~iter:(buffer#get_iter `START) template
+ buffer#insert ~iter:(buffer#get_iter `START) template;
+ filename <- None;
+ buffer#set_modified false;
+ set_star self#ppFilename false
method goto (pos: [`Top | `Bottom | `Cursor]) () =
match pos with
in
dowhile (getpos ());
self#notify
- with Margin -> ())
+ with Margin -> self#notify)
| `Cursor ->
let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
let cursor_iter () = buffer#get_iter_at_mark `INSERT in
(back_until_cursor (); self#notify)
else (* cursor = locked *)
()
- with Margin -> ())
+ with Margin -> self#notify)
method onGoingProof () =
match self#status.proof_status with