From a936e9ae133f103ed9f781a7aa363c0006a2f178 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 8 Aug 2013 18:52:13 +0000 Subject: 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 --- ide/session.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'ide/session.ml') 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 -- cgit v1.2.3