lib/future: computations that are Exn can be replaced

A computation that is an exception morally holds no value
hence can be replaced by an type-equivalent computation.
This mechanism is used to edit broken proofs.
lib/dag: various improvements

- clusters can hold some data
- edges and nodes can be deleted
lib/vcs: various improvements

- gc function to clear unreferenced nodes
- utility function to get the ancestors of a commit
- utility function to edit a merge commit
lib/cstack: various improvements

- renaming reflecting the semantic of functions
- ability to edit the stack at the top of a _focused_zone_
CoqIDE protocol/serialization revised

- both requests and responses are serialized using the same generic code
- no more interp message.  Replaced by:
  - query: performs a query (Search/Check...) at a given state
  - add: adds to the document a new sentence at the current edit point
  - edit_at: changes the edit point.  the result could be a rewind _or_
    a focus to a specific zone that can be edited without rewinding the
    whole document
fake_ide ported to the new protocol (FIXME tests fail)
CoqIDE ported to the revides protocol (FIXME some XXX)

- the zone to be edited is now between the marks
  start_of_input and stop_of_input
- when -debug is given, the edit zone is underlined
- the cmd_stack is focused/unfocused according to the new protocol
- read only tag resurrected and used to block the "Qed" ending
  a focused zone
STM: some refactoring, support revised CoqIDE protocol (TODO XXX)
fixtest