aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqOps.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-01 15:35:28 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-01 15:35:28 +0000
commit56319aaf096cbb6061ae310ac36583fbd61a3d13 (patch)
tree6a33bcdfa96c398c399f79bdd555613214f6d7b2 /ide/coqOps.ml
parent51798358c936ae3276a68d5045acb71023619cfb (diff)
CoqIDE: fix reset initial
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16824 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqOps.ml')
-rw-r--r--ide/coqOps.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 92b2a5e74..0dea01cd5 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -725,6 +725,9 @@ object(self)
buffer#delete_mark phrase.start;
buffer#delete_mark phrase.stop
done;
+ List.iter
+ (buffer#remove_tag ~start:buffer#start_iter ~stop:buffer#end_iter)
+ Tags.Script.all;
(* reset the buffer *)
buffer#move_mark ~where:buffer#start_iter (`NAME "start_of_input");
buffer#move_mark ~where:buffer#end_iter (`NAME "stop_of_input");