diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqOps.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 5769415ad..be0cf9512 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -645,7 +645,11 @@ object(self) messages#clear; messages#push Error msg; ignore(self#process_feedback ()); - self#backtrack_until ~move_insert:false (fun _ id _ _ -> id = Some safe_id) + Coq.seq + (self#backtrack_until ~move_insert:false + (fun _ id _ _ -> id = Some safe_id)) + (Coq.lift (fun () -> + script#scroll_mark_onscreen (`NAME "start_of_input"))) method backtrack_last_phrase = let until n _ _ _ = n >= 1 in @@ -668,7 +672,6 @@ object(self) then self#process_until_iter point else self#backtrack_to_iter ~move_insert:false point) - method tactic_wizard l = let insert_phrase phrase tag = let stop = self#get_start_of_input in |