--- a/src/Pure/Concurrent/future.ML Wed Jan 16 20:40:50 2013 +0100
+++ b/src/Pure/Concurrent/future.ML Wed Jan 16 20:41:29 2013 +0100
@@ -55,6 +55,8 @@
val interruptible_task: ('a -> 'b) -> 'a -> 'b
val cancel_group: group -> unit
val cancel: 'a future -> unit
+ val error_msg: Position.T -> (serial * string) * string option -> unit
+ val identify_result: Position.T -> 'a Exn.result -> 'a Exn.result
type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
val default_params: params
val forks: params -> (unit -> 'a) list -> 'a future list
@@ -433,14 +435,24 @@
fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
-(* future jobs *)
+(* results *)
+
+fun error_msg pos ((serial, msg), exec_id) =
+ if is_none exec_id orelse exec_id = Position.get_id pos
+ then Output.error_msg' (serial, msg) else warning msg;
-fun assign_result group result raw_res =
+fun identify_result pos res =
+ (case res of
+ Exn.Exn exn =>
+ let val exec_id =
+ (case Position.get_id pos of
+ NONE => []
+ | SOME id => [(Markup.exec_idN, id)])
+ in Exn.Exn (Par_Exn.identify exec_id exn) end
+ | _ => res);
+
+fun assign_result group result res =
let
- val res =
- (case raw_res of
- Exn.Exn exn => Exn.Exn (Par_Exn.identify [] exn)
- | _ => raw_res);
val _ = Single_Assignment.assign result res
handle exn as Fail _ =>
(case Single_Assignment.peek result of
@@ -453,6 +465,9 @@
| Exn.Res _ => true);
in ok end;
+
+(* future jobs *)
+
fun future_job group interrupts (e: unit -> 'a) =
let
val result = Single_Assignment.var "future" : 'a result;
@@ -467,7 +482,7 @@
then Multithreading.private_interrupts else Multithreading.no_interrupts)
(fn _ => Position.setmp_thread_data pos e ())) ()
else Exn.interrupt_exn;
- in assign_result group result res end;
+ in assign_result group result (identify_result pos res) end;
in (result, job) end;
@@ -563,7 +578,7 @@
val task = Task_Queue.dummy_task;
val group = Task_Queue.group_of_task task;
val result = Single_Assignment.var "value" : 'a result;
- val _ = assign_result group result res;
+ val _ = assign_result group result (identify_result (Position.thread_data ()) res);
in Future {promised = false, task = task, result = result} end;
fun value x = value_result (Exn.Res x);
@@ -619,7 +634,9 @@
else
let
val group = Task_Queue.group_of_task task;
- fun job ok = assign_result group result (if ok then res else Exn.interrupt_exn);
+ val pos = Position.thread_data ();
+ fun job ok =
+ assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn);
val _ =
Multithreading.with_attributes Multithreading.no_interrupts (fn _ =>
let