match status.proof_status with
| Incomplete_proof (_, goal) when goal <> user_goal ->
goal_changed := true;
- MatitaEngine.eval_ast status (goal_ast user_goal)
+ MatitaEngine.eval_ast
+ ~do_heavy_checks:true status (goal_ast user_goal)
| _ -> status
in
- let new_status = MatitaEngine.eval_ast status st in
+ let new_status = MatitaEngine.eval_ast ~do_heavy_checks:true status st in
let new_aliases =
match ex with
| TA.Command (_, TA.Alias _)
(** goal as seen by the user (i.e. metano corresponding to current tab) *)
val mutable userGoal = ~-1
-
+ val mutable lock_mark_pos = 0
(** text mark and tag representing locked part of a script *)
val locked_mark =
try
self#_advance ?statement ();
self#notify
- with Margin -> self#notify
+ with
+ | Margin -> self#notify
+ | exc -> self#notify; raise exc
method retract () =
try
self#_retract ();
self#notify
- with Margin -> self#notify
+ with
+ | Margin -> self#notify
+ | exc -> self#notify; raise exc
method private getFuture =
buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark))
~stop:buffer#end_iter ()
+
(** @param rel_offset relative offset from current position of locked_mark *)
method private moveMark rel_offset =
let mark = `MARK locked_mark in
in
buffer#move_mark mark ~where:new_mark_pos;
buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos;
+ lock_mark_pos <- new_mark_pos#offset;
buffer#move_mark `INSERT old_insert;
begin
match self#status.proof_status with
end ;
while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
+ method clean_dirty_lock =
+ let lock_mark_iter = buffer#get_iter (`OFFSET lock_mark_pos) in
+ buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
+ buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:lock_mark_iter
+
val mutable observers = []
method addObserver (o: MatitaTypes.status -> unit) =
observers <- o :: observers
method private notify =
-prerr_endline ("************* NOTIFICATO");
let status = self#status in
List.iter (fun o -> o status) observers
in
dowhile (getpos ());
self#notify
- with Margin -> self#notify)
+ with
+ | Margin -> self#notify
+ | exc -> self#notify; raise exc)
| `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 -> self#notify)
-
+ with
+ | Margin -> self#notify
+ | exc -> self#notify; raise exc)
+
method onGoingProof () =
match self#status.proof_status with
| No_proof | Proof _ -> false