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
Clib: fold_left_until added to CList

CStack just calls it to implement fold_until.
CSig.seek renamed CSig.until, since there is no seek function.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16867 85f007b7-540e-0410-9357-904b9bb8a0f7
STM: add "Stm Wait" to wait for the slaves to complete their jobs

Used by fake_ide, that before editing a broken proof has to be sure
Coq known the proof is broken.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16868 85f007b7-540e-0410-9357-904b9bb8a0f7
STM: a proof with nested proofs cannot be delegated

The reason is that the state gets altered by side effects
by the Qed of inner proofs.  This kind of side effects cannot
be reproduced in the slaves easily.  And there is no point
in working hard for this corner case.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16869 85f007b7-540e-0410-9357-904b9bb8a0f7
CoqIDE: move cmd_stack to a separate module: Document

The idea is to move the logic related to document handling
to a separate module that can be tested by fake_ide too.
CoqOps should "only" interface Document with the GtkTextBuffer.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16870 85f007b7-540e-0410-9357-904b9bb8a0f7
fake_ide: ported to Document + 2 tests for editing a proof (locally)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16871 85f007b7-540e-0410-9357-904b9bb8a0f7
CoqIDE: ported to Document

The code is simpler, but there is still room for improvement.
In particular find_id (implemented in both coqOps and fake_id)
should be part of Document.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16872 85f007b7-540e-0410-9357-904b9bb8a0f7