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, 8 insertions, 6 deletions

diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index ec759b67f..a95b9f892 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -8,7 +8,9 @@
 
 open Preferences
 
-class command_window coqtop =
+class command_window coqtop
+  ~mark_as_broken ~mark_as_processed ~cur_state
+=
 (*  let window = GWindow.window
 		 ~allow_grow:true ~allow_shrink:true
 		 ~width:500 ~height:250
@@ -114,14 +116,14 @@ object(self)
       let log level message = result#buffer#insert (message^"\n") in
       let process =
 	Coq.bind (Coq.interp ~logger:log ~raw:true 0 phrase) (function
-          | Interface.Fail (l,str) ->
-            result#buffer#insert ("Error while interpreting "^phrase^":\n"^str);
+          | Interface.Fail (_,l,str) ->
+            result#buffer#insert str;
 	    Coq.return ()
-          | Interface.Good res ->
-            result#buffer#insert ("Result for command " ^ phrase ^ ":\n" ^ res);
+          | Interface.Good (_,res) ->
+            result#buffer#insert res; 
 	    Coq.return ())
       in
-      result#buffer#set_text "";
+      result#buffer#set_text ("Result for command " ^ phrase ^ ":\n");
       Coq.try_grab coqtop process ignore
     in
     ignore (combo#entry#connect#activate ~callback:(on_activate callback));