From 6ba0b48cb9e6a399d4519d40bc65a658d99a3c13 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 21 Jul 2005 16:32:20 +0000 Subject: [PATCH] Regression fixed: goto used to stop (again!) to the new cursor position when 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). --- helm/matita/matitaScript.ml | 78 ++++++++++++++++++++++++------------- 1 file changed, 51 insertions(+), 27 deletions(-) diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 7e4dcb9fc..86775f292 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -594,55 +594,79 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; 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 match pos with - | `Top -> self#goto_top; self#notify + | `Top -> dispose_old_locked_mark (); self#goto_top; self#notify | `Bottom -> (try - let rec dowhile pos = + let rec dowhile () = self#_advance (); - 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 in - dowhile (getoffset ()); + dowhile (); + dispose_old_locked_mark (); self#notify with - | Margin -> self#notify - | exc -> self#notify; raise exc) + | Margin -> dispose_old_locked_mark (); self#notify + | exc -> dispose_old_locked_mark (); self#notify; raise exc) | `Cursor -> - 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 rec aux oldpos = + let rec aux () = self#_advance (); - if (locked_offset ()) - cursor_offset () < 0 && - oldpos - (getoffset ()) < 0 + if cmp () < 0 && (getoldpos ())#compare (getpos ()) < 0 then - aux (getoffset ()) + begin + buffer#move_mark old_locked_mark (getpos ()); + aux () + end in - aux (getoffset ()) + aux () 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 - 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 (); with - | 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 -- 2.39.2