diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-10 11:22:47 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-10 11:22:47 +0000 |
| commit | a8e4bc45bad59f24cddc6c10be83be2d14c1bc57 (patch) | |
| tree | 398f296669442b91e55c6b529b62e9ea7f07eea0 /ide/sentence.ml | |
| parent | 26d5b958417be3750bd767ede0128510fe8508b8 (diff) | |
CoqIDE: a comment is not a sentence
This simplifies the whole document business: the document on the Coq
side has the very same nodes as the CoqIDE document, there are no "fake"
nodes in the CoqIDE document to be skipped over.
We keep the comment tag stamped by the coq_lexer module, since we may
want to allow edits in there without telling Coq (as proof general
does). Not implemented yet, but doable thanks to the comment tag.
Pierre Boutillier suggested that this makes back-1-sentence ugly, since
it moves the cursor far away if the sentence begins with a comment.
While this is true, *today*, there is no need to undo the last sentence
with the button to edit the text. One can just move the cursor where he
likes and edit. In this case the sentence is backtracked automatically
and the cursor is left where it is.
Hence considering initial comments as part of the following sentence
should not be an usability issue anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16866 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/sentence.ml')
| -rw-r--r-- | ide/sentence.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/sentence.ml b/ide/sentence.ml index 7b98d5296..7706c8d34 100644 --- a/ide/sentence.ml +++ b/ide/sentence.ml @@ -35,7 +35,7 @@ let rec backward_search cond (iter:GText.iter) = else backward_search cond iter#backward_char let is_sentence_end s = - s#has_tag Tags.Script.sentence || s#has_tag Tags.Script.comment_sentence + s#has_tag Tags.Script.sentence let is_char s c = s#char = Char.code c |