aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/document.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-24 15:41:37 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-24 15:41:37 +0000
commit7bded288b7727625ee353af5a142ecba15d57240 (patch)
tree843bedb30c5b7c9bf86ae762a93d57102ab6f0f2 /ide/document.ml
parent62e3d6b5f71d17fd4ef683d9f36461d9d16b1a6c (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/document.ml')
-rw-r--r--ide/document.ml4
1 files changed, 2 insertions, 2 deletions
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