# HG changeset patch
# User wenzelm
# Date 1278354999 -7200
# Node ID f1ea60bb7754dd5119aec0d240cc2b79298769d8
# Parent  3f499df0751f71d7665fc3d017a845e6bd03916e
async_state: report within proper transaction context;

diff -r 3f499df0751f -r f1ea60bb7754 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jul 05 14:35:00 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Jul 05 20:36:39 2010 +0200
@@ -563,8 +563,10 @@
 
 fun async_state (tr as Transition {print, ...}) st =
   if print then
-    ignore (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
-      (fn () => Future.report (setmp_thread_position tr (fn () => print_state false st))))
+    ignore
+      (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
+        (fn () =>
+          setmp_thread_position tr (fn () => Future.report (fn () => print_state false st)) ()))
   else ();
 
 fun error_msg tr exn_info =