(** 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 =
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) =