# HG changeset patch
# User wenzelm
# Date 1278270082 -7200
# Node ID b16231572c610fdb1ebc817770c5317240418697
# Parent  628eabe2213a875b26e631205351892e42368859
general Future.report -- also for Toplevel.async_state;

diff -r 628eabe2213a -r b16231572c61 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sun Jul 04 00:05:32 2010 +0200
+++ b/src/Pure/Concurrent/future.ML	Sun Jul 04 21:01:22 2010 +0200
@@ -59,6 +59,7 @@
   val cancel_group: group -> unit
   val cancel: 'a future -> unit
   val shutdown: unit -> unit
+  val report: (unit -> 'a) -> 'a
 end;
 
 structure Future: FUTURE =
@@ -523,6 +524,16 @@
   else ();
 
 
+(* report markup *)
+
+fun report e =
+  let
+    val _ = Output.status (Markup.markup Markup.forked "");
+    val x = e ();  (*sic -- report "joined" only for success*)
+    val _ = Output.status (Markup.markup Markup.joined "");
+  in x end;
+
+
 (*final declarations of this structure!*)
 val map = map_future;
 
diff -r 628eabe2213a -r b16231572c61 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Jul 04 00:05:32 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sun Jul 04 21:01:22 2010 +0200
@@ -563,8 +563,8 @@
 
 fun async_state (tr as Transition {print, ...}) st =
   if print then
-    ignore (Future.fork_group (Task_Queue.new_group (Future.worker_group ())) (fn () =>
-      setmp_thread_position tr (fn () => print_state false st) ()))
+    ignore (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
+      (fn () => Future.report (setmp_thread_position tr (fn () => print_state false st))))
   else ();
 
 fun error_msg tr exn_info =
diff -r 628eabe2213a -r b16231572c61 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sun Jul 04 00:05:32 2010 +0200
+++ b/src/Pure/goal.ML	Sun Jul 04 21:01:22 2010 +0200
@@ -104,12 +104,7 @@
 
 (* parallel proofs *)
 
-fun fork e = Future.fork_pri ~1 (fn () =>
-  let
-    val _ = Output.status (Markup.markup Markup.forked "");
-    val x = e ();  (*sic*)
-    val _ = Output.status (Markup.markup Markup.joined "");
-  in x end);
+fun fork e = Future.fork_pri ~1 (fn () => Future.report e);
 
 val parallel_proofs = Unsynchronized.ref 1;