Coqide ported to STM

Main changes for STM:
1) protocol changed to carry edit/state ids
2) colouring reflects the actual status of every span (evaluated or not)
3) button to force the evaluation of the whole buffer
4) cmd_stack and backtracking completely changed to use state numbers
   instead of counting sentences
5) feedback messages are completely asynchronous, and the whole protocol
   could be made so with a minor effort, but there is little point in it
   right now.  Left as a future improvement.  Missing bit: add
   sentence-id to responses of interp command.

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

1 files changed, 7 insertions, 4 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index c3cef6cda..331408b6d 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -375,12 +375,15 @@ let set_logger l = logger := l
 (** Feedback *)
 
 let feeder = ref ignore
-let feedback_id = ref 0
+let feedback_id = ref (Interface.Edit 0)
 let set_id_for_feedback i = feedback_id := i
-let feedback what =
+let feedback ?state_id what =
   !feeder {
-     Interface.edit_id = !feedback_id;
-     Interface.content = what
+     Interface.content = what;
+     Interface.id =
+       match state_id with
+       | Some id -> Interface.State id
+       | None -> !feedback_id;
   }
 let set_feeder f = feeder := f