Fixing CAMLP4 compilation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16865 85f007b7-540e-0410-9357-904b9bb8a0f7
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
Document: undoing inside a focused zone does not require unfocusing

To test this fake_ide has also been improved with the GOALS command.
As for CoqIDE, ADDing a sentence does not force its evaluation.
The "advance 1 sentence" button is an ADD + GOALS.  If one of the
ADDed sentences is wrong, GOALS receives the error.  The GUI then
backtracks to a safe state id (sent by Coq).

fake_ide has GOALS (asserts that the goals call was OK) and FAILGOALS
to assert it fails and backtrack to a valid state. see unfdo022.fake.

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

Many things were wrong.  Error tags were deleted by mistake, the
screen was recentered on `INSERT using the wrong function (that cause
some horizontal scrolling even if it was not needed), the
cursor not advanced to the end of the wrong sentence.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16874 85f007b7-540e-0410-9357-904b9bb8a0f7
CoqIDE: single underline for errors

The double underline has some bugs, sometimes the lower line
is not correctly cleared.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16875 85f007b7-540e-0410-9357-904b9bb8a0f7
Dag: some comments on the concept of cluster

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16876 85f007b7-540e-0410-9357-904b9bb8a0f7
Vcs: the gc method returns the set of nodes that were collected

In this way one can post-process them.  Stm can for example cancel
the ongoing jobs related to nodes that are no more there.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16877 85f007b7-540e-0410-9357-904b9bb8a0f7
STM: cancel slaves working on outdated jobs

I did not manage to make the slave manager use Unix.select to wait for a
response from the slave for a limited time and check for cancellation.

Hence the following semi-cooperative model:
- The slave has a thread that sends a Tick every second when the thread
  is working
- The slave_manager will then be unblocked periodically by this tick and
  check for cancellation
- Cancellation is, for the moment, implemented using kill.

To kill a process on windows one could bind TerminateProcess (>= WinXP)
or RegisterWindowMessage + BroadcastSystemMessage (>= Win2k).

See: http://msdn.microsoft.com/en-us/library/windows/desktop/ms686722%28v=vs.85%29.aspx

Another option is to make the slave_manager send to the tick thread on
the slave process a boolean answer to the Tick message, and the tick
thread could eventually bail out.  But to do that, it is way better
to have a second channel, used only by this tick thread.  This solution
sound very like the one proposed for windows, but requires more work.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16879 85f007b7-540e-0410-9357-904b9bb8a0f7
STM: prefix debug messages with slave-id

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16880 85f007b7-540e-0410-9357-904b9bb8a0f7
CoqIDE: make error background configurable

#FFCCCC is quite dark on some beamers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16881 85f007b7-540e-0410-9357-904b9bb8a0f7
Getting rid of the use of deprecated elements (from the OCaml standard library).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove some uses of local modules (some were unused, some were costly).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16883 85f007b7-540e-0410-9357-904b9bb8a0f7
Avoid polymorphic comparison (coqdoc).

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