diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-24 15:41:37 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-24 15:41:37 +0000 |
| commit | 7bded288b7727625ee353af5a142ecba15d57240 (patch) | |
| tree | 843bedb30c5b7c9bf86ae762a93d57102ab6f0f2 /ide | |
| parent | 62e3d6b5f71d17fd4ef683d9f36461d9d16b1a6c (diff) | |
CoqIDE: fix coloring bug when jumping back to the first phrase
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16928 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqOps.ml | 4 | ||||
| -rw-r--r-- | ide/document.ml | 4 |
2 files changed, 5 insertions, 3 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index eb09d3bbb..59c399842 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -553,7 +553,8 @@ object(self) (* finds the state_id and if it an unfocus is needed to reach it *) method private find_id until = - try Doc.find_id document (fun id { start;stop } -> until (Some id) start stop) + try + Doc.find_id document (fun id { start;stop } -> until (Some id) start stop) with Not_found -> initial_state, Doc.focused document method private cleanup seg = @@ -586,6 +587,7 @@ object(self) buffer#remove_tag Tags.Script.tooltip ~start ~stop; buffer#remove_tag Tags.Script.processed ~start ~stop; buffer#remove_tag Tags.Script.to_process ~start ~stop; + buffer#remove_tag Tags.Script.unjustified ~start ~stop; self#show_goals in Coq.bind (Coq.lift opening) (fun () -> let rec undo to_id unfocus_needed = diff --git a/ide/document.ml b/ide/document.ml index fab318f18..deb780739 100644 --- a/ide/document.ml +++ b/ide/document.ml @@ -123,11 +123,11 @@ let assign_tip_id d id = let cut_at d id = let aux (n, zone) { state_id; data } = - if stateid_opt_equal state_id (Some id) then CSig.Stop (n, List.rev zone) + if stateid_opt_equal state_id (Some id) then CSig.Stop (n, zone) else CSig.Cont (n + 1, data :: zone) in let n, zone = CList.fold_left_until aux (0, []) d.stack in for i = 1 to n do ignore(pop d) done; - zone + List.rev zone let find_id d f = let top, focus, bot = to_lists d in |