diff -r 1261481ef5e5 -r 8248cda328de src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Aug 31 23:28:21 2010 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 31 23:46:49 2010 +0200
@@ -192,6 +192,59 @@
 
 
 
+(* toplevel transactions *)
+
+local
+
+fun proof_status tr st =
+  (case try Toplevel.proof_of st of
+    SOME prf => Toplevel.status tr (Proof.status_markup prf)
+  | NONE => ());
+
+fun async_state tr st =
+  if Toplevel.print_of tr then
+    ignore
+      (Future.fork
+        (fn () =>
+          Toplevel.setmp_thread_position tr
+            (fn () => Future.status (fn () => Toplevel.print_state false st)) ()))
+  else ();
+
+in
+
+fun run_command thy_name tr st =
+  (case
+      (case Toplevel.init_of tr of
+        SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
+      | NONE => Exn.Result ()) of
+    Exn.Result () =>
+      let
+        val int = is_some (Toplevel.init_of tr);
+        val (errs, result) =
+          (case Toplevel.transition int tr st of
+            SOME (st', NONE) => ([], SOME st')
+          | SOME (_, SOME exn_info) =>
+              (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
+                [] => raise Exn.Interrupt
+              | errs => (errs, NONE))
+          | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
+        val _ = List.app (Toplevel.error_msg tr) errs;
+        val _ =
+          (case result of
+            NONE => Toplevel.status tr Markup.failed
+          | SOME st' =>
+             (Toplevel.status tr Markup.finished;
+              proof_status tr st';
+              if int then () else async_state tr st'));
+      in result end
+  | Exn.Exn exn =>
+     (Toplevel.error_msg tr (ML_Compiler.exn_message exn); Toplevel.status tr Markup.failed; NONE))
+
+end;
+
+
+
+
 (** editing **)
 
 (* edit *)
@@ -214,7 +267,7 @@
           NONE => NONE
         | SOME st =>
             let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr)
-            in Toplevel.run_command name exec_tr st end));
+            in run_command name exec_tr st end));
     val state' = define_exec exec_id' exec' state;
   in (exec_id', (id, exec_id') :: updates, state') end;