changeset 39391 | f1d6ede54862 |
parent 39238 | 7189a138dd6c |
child 40390 | 5bc4336d9768 |
--- a/src/Pure/PIDE/document.ML Wed Sep 15 16:04:40 2010 +0200 +++ b/src/Pure/PIDE/document.ML Wed Sep 15 16:06:52 2010 +0200 @@ -204,10 +204,10 @@ fun async_state tr st = if Toplevel.print_of tr then ignore - (Future.fork + (Future.fork_group (Task_Queue.new_group NONE) (fn () => Toplevel.setmp_thread_position tr - (fn () => Future.status (fn () => Toplevel.print_state false st)) ())) + (fn () => Toplevel.print_state false st) ())) else (); in