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/tags.mli | |
| 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/tags.mli')
| -rw-r--r-- | ide/tags.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/tags.mli b/ide/tags.mli index f79ae1f11..3c5900269 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -9,7 +9,7 @@ module Script : sig val table : GText.tag_table - val comment_sentence : GText.tag + val comment : GText.tag val error : GText.tag val error_bg : GText.tag val to_process : GText.tag |