From aadff10ea8da78a9acc76a3dc595e47cfa5b72cf Mon Sep 17 00:00:00 2001
From: vgross
Date: Mon, 31 May 2010 22:22:13 +0000
Subject: CoqIDE goes multiprocess

This commit changes many things in CoqIDE, and several breakage are to
be expected. So far, evaluation in standard tactic mode and backtracking
seems to be working.

Future work :
- clean up the thread management crud remaining in ide/coqide.ml
- rework the exception handling
- rework the init system in Coqtop

plus many other things

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13043 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/command_windows.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'ide/command_windows.ml')

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index beb8ebb526..1b768de9a2 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+let get_current_toplevel = ref (fun () -> Coq.dummy_coqtop)
+
 class command_window () =
 (*  let window = GWindow.window
 		 ~allow_grow:true ~allow_shrink:true
@@ -104,9 +106,10 @@ object(self)
 	then com ^ " " else com ^ " " ^ entry#text ^" . "
       in
       try
-	Coq.raw_interp Coq.dummy_coqtop phrase;
+        let curtop = !get_current_toplevel () in
+	Coq.raw_interp curtop phrase;
 	result#buffer#set_text
-	  ("Result for command " ^ phrase ^ ":\n" ^ (Coq.read_stdout Coq.dummy_coqtop))
+	  ("Result for command " ^ phrase ^ ":\n" ^ (Coq.read_stdout curtop))
       with e ->
 	let (s,loc) = Coq.process_exn e in
 	assert (Glib.Utf8.validate s);
-- 
cgit v1.2.3