Coqide: restore the tag removal of copy-pasted zones

 The handler for apply_tag removed in commit 16044 was probaly meant
 for that. We now proceed in a more simple way, in Sentence.split_slice_lax,
 instead of doing a remove_tag in a apply_tag handler (!).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16058 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 7 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 6d99077bea..c1f1675177 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -329,13 +329,8 @@ object(self)
       buffer#delete_mark phrase.stop
     done;
     (* reset the buffer *)
-    let start = buffer#start_iter in
-    let stop = buffer#end_iter in
-    buffer#move_mark ~where:start (`NAME "start_of_input");
-    buffer#remove_tag Tags.Script.processed ~start ~stop;
-    buffer#remove_tag Tags.Script.unjustified ~start ~stop;
-    buffer#remove_tag Tags.Script.to_process ~start ~stop;
-    Sentence.tag_on_insert buffer;
+    buffer#move_mark ~where:buffer#start_iter (`NAME "start_of_input");
+    Sentence.tag_all buffer;
     (* clear the views *)
     messages#clear;
     proof#clear ();