From c91c06bd374f5edbed5c562d7fb1858058307a7a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 18 Jul 2005 16:48:43 +0000 Subject: [PATCH] Bug fixed: clicking on a new position while advancing/retracting now does absolutely nothing (i.e. at the very end of the execution the cursor is at the end of the blue area). --- helm/matita/matitaScript.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index e0e4227dd..c2b9a7e93 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -611,12 +611,12 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; | 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 - let cmp = (locked_iter ())#offset - (cursor_iter ())#offset in + let cursor_iter = buffer#get_iter_at_mark `INSERT in + let cmp = (locked_iter ())#offset - cursor_iter#offset in let forward_until_cursor () = (* go forward until locked > cursor *) let rec aux oldpos = self#_advance (); - if (locked_iter ())#compare (cursor_iter ()) < 0 && + if (locked_iter ())#compare cursor_iter < 0 && oldpos#compare (getpos ()) < 0 then aux (getpos ()) -- 2.39.2