STM: not optimize proofs containing an Undo

Actually we could, but we should check the state one jumps to is
inside the proof...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16889 85f007b7-540e-0410-9357-904b9bb8a0f7
Summary: if an unfreeze function fails, print an error message

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

Ideally all unmarshallable content in the state should be
stocked using Ephemeron keys.  In this way the state becomes
always marshallable (because the unmarshallable content is magically
dropped).  The mli contains more detailed doc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16891 85f007b7-540e-0410-9357-904b9bb8a0f7
Future: ported to Ephemeron + exception enhancing

A future always carries a fix_exn with it: a function that enriches
an exception with the state in which the error occurs and also a safe
state close to it where one could backtrack.

A future can be in two states: Ongoing or Finished.
The latter state is obtained by Future.join and after that the future
can be safely marshalled.
An Ongoing future can be marshalled, but its value is lost.  This makes
it possible to send the environment to a slave process without
pre-processing it to drop all unfinished proofs (they are dropped
automatically in some sense).

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

Ideally, any component of the global state that is a function or any
other unmarshallable data should be stocked as an ephemeron to make
the state always marshallable.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16893 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqtop: fix looping over a broken state.

Coqtop is not able to deal with broken states, hence Stm.interp
has to immediately backtrack to the last meaningful state.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16894 85f007b7-540e-0410-9357-904b9bb8a0f7
proof modes: use ephemerons to represent them in proof state

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16895 85f007b7-540e-0410-9357-904b9bb8a0f7
ideutils: support custom size for stock icons

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16896 85f007b7-540e-0410-9357-904b9bb8a0f7
wg_Commands: smaller icons in tabs

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

To tell the gui what a slave is doing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16898 85f007b7-540e-0410-9357-904b9bb8a0f7
STM: send the gui the status of the slaves

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16899 85f007b7-540e-0410-9357-904b9bb8a0f7
CoqIDE: display in the errors window also the slaves status

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16900 85f007b7-540e-0410-9357-904b9bb8a0f7
Wg_Commands: when detached display the buffer name

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16901 85f007b7-540e-0410-9357-904b9bb8a0f7
Wg_Commands: fix warning "widget not within a GtkWindow"

The constructor was calling indirectly grab_default that requires
the widget to be anchored.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16902 85f007b7-540e-0410-9357-904b9bb8a0f7
wg_Detachable: move out of wg_Command

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16903 85f007b7-540e-0410-9357-904b9bb8a0f7
Wg_Find: regex + case insensitive find/replace support

It uses Str, hence it also supports captures \(..\) and \1 .. \n

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16904 85f007b7-540e-0410-9357-904b9bb8a0f7
emacs config: next-error search path ok even if default-directory unset.
This way next-error behaves accordingly with make -C. Making the setting
of default-directory independent of the compile/next-error setting.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16905 85f007b7-540e-0410-9357-904b9bb8a0f7
CoqIDE: do not try to backtrack to a dummy id

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16906 85f007b7-540e-0410-9357-904b9bb8a0f7
CoqIDE: always retag on insert

This should fix Arnaud's bug (reported by private email) that makes
coq eat two sentences at once (and process only the first one).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16907 85f007b7-540e-0410-9357-904b9bb8a0f7
STM: do not enrich exceptions more than once

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