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, 2 insertions, 2 deletions

diff --git a/ide/tags.ml b/ide/tags.ml
index de3287720..556430aaf 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -19,7 +19,7 @@ let processing_color = ref "light blue"
 module Script =
 struct
   let table = GText.tag_table ()
-  let comment_sentence = make_tag table ~name:"comment_sentence" []
+  let comment = make_tag table ~name:"comment" []
   let error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"]
   let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND "#FFCCCC"]
   let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color]
@@ -30,7 +30,7 @@ struct
   let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *)
 
   let all =
-     [comment_sentence; error; error_bg; to_process; processed; unjustified;
+     [comment; error; error_bg; to_process; processed; unjustified;
      found; sentence; tooltip]
 
   let edit_zone =