async_state: report within proper transaction context;
authorwenzelm
Mon Jul 05 20:36:39 2010 +0200 (2010-07-05 ago)
changeset 37711f1ea60bb7754
parent 37710 3f499df0751f
child 37712 7f25bf4b4bca
async_state: report within proper transaction context;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Jul 05 14:35:00 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Jul 05 20:36:39 2010 +0200
     1.3 @@ -563,8 +563,10 @@
     1.4  
     1.5  fun async_state (tr as Transition {print, ...}) st =
     1.6    if print then
     1.7 -    ignore (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
     1.8 -      (fn () => Future.report (setmp_thread_position tr (fn () => print_state false st))))
     1.9 +    ignore
    1.10 +      (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
    1.11 +        (fn () =>
    1.12 +          setmp_thread_position tr (fn () => Future.report (fn () => print_state false st)) ()))
    1.13    else ();
    1.14  
    1.15  fun error_msg tr exn_info =