diff options
| -rw-r--r-- | ide/coqOps.ml | 9 | ||||
| -rw-r--r-- | ide/sentence.ml | 6 | ||||
| -rw-r--r-- | ide/sentence.mli | 2 | ||||
| -rw-r--r-- | ide/tags.ml | 3 | ||||
| -rw-r--r-- | ide/tags.mli | 1 |
5 files changed, 10 insertions, 11 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 6d99077be..c1f167517 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 5c61f98de..f6bc99207 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 c552024f4..2a83d04f7 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 cde831513..3d0e873a7 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 a96ae98b9..2d74d43f2 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 : |