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

5 files changed, 10 insertions, 11 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 ();
diff --git a/ide/sentence.ml b/ide/sentence.ml
index 5c61f98dec..f6bc99207a 100644
--- a/ide/sentence.ml
+++ b/ide/sentence.ml
@@ -14,8 +14,7 @@
     an unterminated sentence. *)
 
 let split_slice_lax (buffer:GText.buffer) start stop =
-  buffer#remove_tag ~start ~stop Tags.Script.comment_sentence;
-  buffer#remove_tag ~start ~stop Tags.Script.sentence;
+  List.iter (buffer#remove_tag ~start ~stop) Tags.Script.all;
   let slice = buffer#get_text ~start ~stop () in
   let mkiter =
     (* caveat : partial application with effects *)
@@ -109,7 +108,8 @@ let tag_on_insert buffer =
     buffer#apply_tag ~start:soi ~stop:soi#forward_char Tags.Script.error
 
 let tag_all buffer =
-  try split_slice_lax buffer buffer#start_iter buffer#end_iter
+  let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in
+  try split_slice_lax buffer soi buffer#end_iter
   with Coq_lex.Unterminated -> ()
 
 (** Search a sentence around some position *)
diff --git a/ide/sentence.mli b/ide/sentence.mli
index c552024f42..2a83d04f7b 100644
--- a/ide/sentence.mli
+++ b/ide/sentence.mli
@@ -10,7 +10,7 @@
 
 val tag_on_insert : GText.buffer -> unit
 
-(** Retag the ends of sentences in the whole buffer *)
+(** Retag the ends of sentences in the non-locked part of the buffer *)
 
 val tag_all : GText.buffer -> unit
 
diff --git a/ide/tags.ml b/ide/tags.ml
index cde831513b..3d0e873a77 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -26,6 +26,9 @@ struct
   let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold";`EDITABLE false]
   let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"]
   let sentence = make_tag table ~name:"sentence" []
+  let all =
+    [comment_sentence; error; to_process; processed; unjustified;
+     found; sentence]
 end
 module Proof =
 struct
diff --git a/ide/tags.mli b/ide/tags.mli
index a96ae98b97..2d74d43f27 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -16,6 +16,7 @@ sig
   val unjustified : GText.tag
   val found : GText.tag
   val sentence : GText.tag
+  val all : GText.tag list
 end
 
 module Proof :