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

1 files changed, 1 insertions, 4 deletions

diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index d1d7c6629..7eb0f28c8 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -45,10 +45,7 @@ and sentence initial stamp = parse
       match comment lexbuf with
         | None -> raise Unterminated
         | Some comm_last ->
-          (* A comment alone is a sentence.
-	     A comment in a sentence doesn't terminate the sentence.
-             Note: comm_end is the position of the comment final ')' *)
-          if initial then stamp comm_last Tags.Script.comment_sentence;
+          stamp comm_last Tags.Script.comment;
           sentence initial stamp lexbuf
     }
   | "\"" {