the user clicks somewhere. The source of the regression was the difficulty of
remembering the position of the marks while the text is modified (by automatic
insertion of aliases). Solved by using ad-hoc temporary marks in place of
iterators (first version tried) and offsets (most recent version tried).
set_star self#ppFilename false
method goto (pos: [`Top | `Bottom | `Cursor]) () =
set_star self#ppFilename false
method goto (pos: [`Top | `Bottom | `Cursor]) () =
- let getoffset () = (buffer#get_iter_at_mark (`MARK locked_mark))#offset in
+ let old_locked_mark =
+ `MARK
+ (buffer#create_mark ~name:"old_locked_mark"
+ ~left_gravity:true (buffer#get_iter_at_mark (`MARK locked_mark))) in
+ let getpos _ = buffer#get_iter_at_mark (`MARK locked_mark) in
+ let getoldpos _ = buffer#get_iter_at_mark old_locked_mark in
+ let dispose_old_locked_mark () = buffer#delete_mark old_locked_mark in
- | `Top -> self#goto_top; self#notify
+ | `Top -> dispose_old_locked_mark (); self#goto_top; self#notify
- let newpos = getoffset () in
- if pos - newpos < 0 then
- dowhile newpos
+ let newpos = getpos () in
+ if (getoldpos ())#compare newpos < 0 then
+ begin
+ buffer#move_mark old_locked_mark newpos;
+ dowhile ()
+ end
- dowhile (getoffset ());
+ dowhile ();
+ dispose_old_locked_mark ();
- | Margin -> self#notify
- | exc -> self#notify; raise exc)
+ | Margin -> dispose_old_locked_mark (); self#notify
+ | exc -> dispose_old_locked_mark (); self#notify; raise exc)
- let locked_offset () =
- (buffer#get_iter_at_mark (`NAME "locked"))#offset in
- let cursor_offset () = (buffer#get_iter_at_mark `INSERT)#offset in
- let cmp = (locked_offset ()) - cursor_offset () in
+ let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
+ let cursor_iter () = buffer#get_iter_at_mark `INSERT in
+ let remember =
+ `MARK
+ (buffer#create_mark ~name:"initial_insert"
+ ~left_gravity:true (cursor_iter ())) in
+ let dispose_remember () = buffer#delete_mark remember in
+ let remember_iter () =
+ buffer#get_iter_at_mark (`NAME "initial_insert") in
+ let cmp () = (locked_iter ())#offset - (remember_iter ())#offset in
+ let icmp = cmp () in
let forward_until_cursor () = (* go forward until locked > cursor *)
let forward_until_cursor () = (* go forward until locked > cursor *)
- if (locked_offset ()) - cursor_offset () < 0 &&
- oldpos - (getoffset ()) < 0
+ if cmp () < 0 && (getoldpos ())#compare (getpos ()) < 0
+ begin
+ buffer#move_mark old_locked_mark (getpos ());
+ aux ()
+ end
in
let rec back_until_cursor len = (* go backward until locked < cursor *)
function
statements, (status::_ as history) when len <= 0 ->
in
let rec back_until_cursor len = (* go backward until locked < cursor *)
function
statements, (status::_ as history) when len <= 0 ->
- self#_retract (cmp - len) status statements history
+ self#_retract (icmp - len) status statements history
| statement::tl1, _::tl2 ->
back_until_cursor (len - String.length statement) (tl1,tl2)
| _,_ -> assert false
in
(try
| statement::tl1, _::tl2 ->
back_until_cursor (len - String.length statement) (tl1,tl2)
| _,_ -> assert false
in
(try
- if cmp < 0 then (* locked < cursor *)
- (forward_until_cursor (); self#notify)
- else if cmp > 0 then (* locked > cursor *)
- (back_until_cursor cmp (statements,history); self#notify)
- else (* cursor = locked *)
- ()
+ begin
+ if icmp < 0 then (* locked < cursor *)
+ (forward_until_cursor (); self#notify)
+ else if icmp > 0 then (* locked > cursor *)
+ (back_until_cursor icmp (statements,history); self#notify)
+ else (* cursor = locked *)
+ ()
+ end ;
+ dispose_remember ();
+ dispose_old_locked_mark ();
- | Margin -> self#notify
- | exc -> self#notify; raise exc)
+ | Margin -> dispose_remember (); dispose_old_locked_mark (); self#notify
+ | exc -> dispose_remember (); dispose_old_locked_mark ();
+ self#notify; raise exc)
method onGoingProof () =
match self#status.proof_status with
method onGoingProof () =
match self#status.proof_status with