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, 3 insertions, 1 deletions

diff --git a/ide/session.ml b/ide/session.ml
index 46780b275..bed0747f3 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -102,6 +102,7 @@ let set_buffer_handlers buffer script =
     let start = get_start () in
     let stop = buffer#end_iter in
     buffer#remove_tag Tags.Script.error ~start ~stop;
+    buffer#remove_tag Tags.Script.error_bg ~start ~stop;
     buffer#remove_tag Tags.Script.tooltip ~start ~stop
   in
   let end_action_cb () =
@@ -152,7 +153,7 @@ let create file coqtop_args =
   let _ = set_buffer_handlers (buffer :> GText.buffer) script in
   let proof = create_proof () in
   let messages = create_messages () in
-  let command = new Wg_Command.command_window coqtop in
+  let command = new Wg_Command.command_window coqtop ~mark_as_broken:(fun _ -> ()) ~mark_as_processed:(fun _ -> ()) ~cur_state:(fun () -> Obj.magic 0) in
   let finder = new Wg_Find.finder (script :> GText.view) in
   let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in
   let _ = fops#update_stats in
@@ -177,6 +178,7 @@ let kill (sn:session) =
   (* To close the detached views of this script, we call manually
      [destroy] on it, triggering some callbacks in [detach_view].
      In a more modern lablgtk, rather use the page-removed signal ? *)
+  sn.coqops#destroy ();
   sn.script#destroy ();
   Coq.close_coqtop sn.coqtop