diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-01 15:35:34 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-01 15:35:34 +0000 |
| commit | 69f73dbbe7bdc3f82adad5f6b2d28d8fa724d562 (patch) | |
| tree | f189fde8b0b544ead37903ea3c82be13654fc8df | |
| parent | 8ef45dfc3f153b123d2a35156dbc0d570f325160 (diff) | |
CoqIDE: when checking the whole document, center script view on error
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16835 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |