From 698a1ca948794ae9509547ddabd57b5f35512f03 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Mon, 30 Sep 2013 16:09:56 +0000 Subject: CoqIDE ported to the revides protocol - the zone to be edited is now between the marks start_of_input and stop_of_input - when -debug is given, the edit zone is underlined - the cmd_stack is focused/unfocused according to the new protocol - read only tag resurrected and used to block the "Qed" ending a focused zone git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16814 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/sentence.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'ide/sentence.ml') diff --git a/ide/sentence.ml b/ide/sentence.ml index 01add490e..7b98d5296 100644 --- a/ide/sentence.ml +++ b/ide/sentence.ml @@ -14,7 +14,8 @@ an unterminated sentence. *) let split_slice_lax (buffer:GText.buffer) start stop = - List.iter (buffer#remove_tag ~start ~stop) Tags.Script.all; + buffer#remove_tag ~start ~stop Tags.Script.sentence; + buffer#remove_tag ~start ~stop Tags.Script.error; let slice = buffer#get_text ~start ~stop () in let apply_tag off tag = (* off is now a utf8-compliant char offset, cf Coq_lex.utf8_adjust *) @@ -98,14 +99,16 @@ let tag_on_insert buffer = found by [grab_ending_dot] to form a non-ending "..". In any case, we retag up to eof, since this isn't that costly. *) if not stop#is_end then - try split_slice_lax buffer start buffer#end_iter + let eoi = buffer#get_iter_at_mark (`NAME "stop_of_input") in + try split_slice_lax buffer start eoi with Coq_lex.Unterminated -> () with StartError -> buffer#apply_tag ~start:soi ~stop:soi#forward_char Tags.Script.error let tag_all buffer = let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in - try split_slice_lax buffer soi buffer#end_iter + let eoi = buffer#get_iter_at_mark (`NAME "stop_of_input") in + try split_slice_lax buffer soi eoi with Coq_lex.Unterminated -> () (** Search a sentence around some position *) -- cgit v1.2.3