1.1 --- a/src/Pure/Concurrent/future.ML	Wed Jan 16 20:40:50 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Jan 16 20:41:29 2013 +0100
     1.3 @@ -55,6 +55,8 @@
     1.4    val interruptible_task: ('a -> 'b) -> 'a -> 'b
     1.5    val cancel_group: group -> unit
     1.6    val cancel: 'a future -> unit
     1.7 +  val error_msg: Position.T -> (serial * string) * string option -> unit
     1.8 +  val identify_result: Position.T -> 'a Exn.result -> 'a Exn.result
     1.9    type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
    1.10    val default_params: params
    1.11    val forks: params -> (unit -> 'a) list -> 'a future list
    1.12 @@ -433,14 +435,24 @@
    1.13  fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
    1.14  
    1.15  
    1.16 -(* future jobs *)
    1.17 +(* results *)
    1.18  
    1.19 -fun assign_result group result raw_res =
    1.20 +fun error_msg pos ((serial, msg), exec_id) =
    1.21 +  if is_none exec_id orelse exec_id = Position.get_id pos
    1.22 +  then Output.error_msg' (serial, msg) else warning msg;
    1.23 +
    1.24 +fun identify_result pos res =
    1.25 +  (case res of
    1.26 +    Exn.Exn exn =>
    1.27 +      let val exec_id =
    1.28 +        (case Position.get_id pos of
    1.29 +          NONE => []
    1.30 +        | SOME id => [(Markup.exec_idN, id)])
    1.31 +      in Exn.Exn (Par_Exn.identify exec_id exn) end
    1.32 +  | _ => res);
    1.33 +
    1.34 +fun assign_result group result res =
    1.35    let
    1.36 -    val res =
    1.37 -      (case raw_res of
    1.38 -        Exn.Exn exn => Exn.Exn (Par_Exn.identify [] exn)
    1.39 -      | _ => raw_res);
    1.40      val _ = Single_Assignment.assign result res
    1.41        handle exn as Fail _ =>
    1.42          (case Single_Assignment.peek result of
    1.43 @@ -453,6 +465,9 @@
    1.44        | Exn.Res _ => true);
    1.45    in ok end;
    1.46  
    1.47 +
    1.48 +(* future jobs *)
    1.49 +
    1.50  fun future_job group interrupts (e: unit -> 'a) =
    1.51    let
    1.52      val result = Single_Assignment.var "future" : 'a result;
    1.53 @@ -467,7 +482,7 @@
    1.54                   then Multithreading.private_interrupts else Multithreading.no_interrupts)
    1.55                  (fn _ => Position.setmp_thread_data pos e ())) ()
    1.56            else Exn.interrupt_exn;
    1.57 -      in assign_result group result res end;
    1.58 +      in assign_result group result (identify_result pos res) end;
    1.59    in (result, job) end;
    1.60  
    1.61  
    1.62 @@ -563,7 +578,7 @@
    1.63      val task = Task_Queue.dummy_task;
    1.64      val group = Task_Queue.group_of_task task;
    1.65      val result = Single_Assignment.var "value" : 'a result;
    1.66 -    val _ = assign_result group result res;
    1.67 +    val _ = assign_result group result (identify_result (Position.thread_data ()) res);
    1.68    in Future {promised = false, task = task, result = result} end;
    1.69  
    1.70  fun value x = value_result (Exn.Res x);
    1.71 @@ -619,7 +634,9 @@
    1.72    else
    1.73      let
    1.74        val group = Task_Queue.group_of_task task;
    1.75 -      fun job ok = assign_result group result (if ok then res else Exn.interrupt_exn);
    1.76 +      val pos = Position.thread_data ();
    1.77 +      fun job ok =
    1.78 +        assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn);
    1.79        val _ =
    1.80          Multithreading.with_attributes Multithreading.no_interrupts (fn _ =>
    1.81            let

     2.1 --- a/src/Pure/Isar/runtime.ML	Wed Jan 16 20:40:50 2013 +0100
     2.2 +++ b/src/Pure/Isar/runtime.ML	Wed Jan 16 20:41:29 2013 +0100
     2.3 @@ -12,6 +12,7 @@
     2.4    exception TOPLEVEL_ERROR
     2.5    val debug: bool Unsynchronized.ref
     2.6    val exn_context: Proof.context option -> exn -> exn
     2.7 +  val exn_messages_ids: (exn -> Position.T) -> exn -> ((serial * string) * string option) list
     2.8    val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
     2.9    val exn_message: (exn -> Position.T) -> exn -> string
    2.10    val debugging: ('a -> 'b) -> 'a -> 'b
    2.11 @@ -42,22 +43,28 @@
    2.12  
    2.13  (* exn_message *)
    2.14  
    2.15 +local
    2.16 +
    2.17  fun if_context NONE _ _ = []
    2.18    | if_context (SOME ctxt) f xs = map (f ctxt) xs;
    2.19  
    2.20 -fun exn_messages exn_position e =
    2.21 +fun identify exn =
    2.22    let
    2.23 -    fun identify exn =
    2.24 -      let val exn' = Par_Exn.identify [] exn
    2.25 -      in (Par_Exn.the_serial exn', exn') end;
    2.26 +    val exn' = Par_Exn.identify [] exn;
    2.27 +    val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
    2.28 +  in ((Par_Exn.the_serial exn', exn'), exec_id) end;
    2.29  
    2.30 -    fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
    2.31 -      | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
    2.32 -      | flatten context exn =
    2.33 -          (case Par_Exn.dest exn of
    2.34 -            SOME exns => maps (flatten context) exns
    2.35 -          | NONE => [(context, identify exn)]);
    2.36 +fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
    2.37 +  | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
    2.38 +  | flatten context exn =
    2.39 +      (case Par_Exn.dest exn of
    2.40 +        SOME exns => maps (flatten context) exns
    2.41 +      | NONE => [(context, identify exn)]);
    2.42  
    2.43 +in
    2.44 +
    2.45 +fun exn_messages_ids exn_position e =
    2.46 +  let
    2.47      fun raised exn name msgs =
    2.48        let val pos = Position.here (exn_position exn) in
    2.49          (case msgs of
    2.50 @@ -66,10 +73,10 @@
    2.51          | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
    2.52        end;
    2.53  
    2.54 -    fun exn_msgs (context, (i, exn)) =
    2.55 +    fun exn_msgs (context, ((i, exn), id)) =
    2.56        (case exn of
    2.57          EXCURSION_FAIL (exn, loc) =>
    2.58 -          map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
    2.59 +          map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id))
    2.60              (sorted_msgs context exn)
    2.61        | _ =>
    2.62          let
    2.63 @@ -94,12 +101,17 @@
    2.64                  raised exn ("THM " ^ string_of_int i)
    2.65                    (msg :: if_context context Display.string_of_thm thms)
    2.66              | _ => raised exn (General.exnMessage exn) []);
    2.67 -        in [(i, msg)] end)
    2.68 +        in [((i, msg), id)] end)
    2.69        and sorted_msgs context exn =
    2.70 -        sort_distinct (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
    2.71 +        sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
    2.72  
    2.73    in sorted_msgs NONE e end;
    2.74  
    2.75 +end;
    2.76 +
    2.77 +fun exn_messages exn_position exn =
    2.78 +  map #1 (exn_messages_ids exn_position exn);
    2.79 +
    2.80  fun exn_message exn_position exn =
    2.81    (case exn_messages exn_position exn of
    2.82      [] => "Interrupt"

     3.1 --- a/src/Pure/ML/ml_compiler.ML	Wed Jan 16 20:40:50 2013 +0100
     3.2 +++ b/src/Pure/ML/ml_compiler.ML	Wed Jan 16 20:41:29 2013 +0100
     3.3 @@ -7,6 +7,7 @@
     3.4  signature ML_COMPILER =
     3.5  sig
     3.6    val exn_position: exn -> Position.T
     3.7 +  val exn_messages_ids: exn -> ((serial * string) * string option) list
     3.8    val exn_messages: exn -> (serial * string) list
     3.9    val exn_message: exn -> string
    3.10    val eval: bool -> Position.T -> ML_Lex.token list -> unit
    3.11 @@ -16,6 +17,7 @@
    3.12  struct
    3.13  
    3.14  fun exn_position _ = Position.none;
    3.15 +val exn_messages_ids = Runtime.exn_messages_ids exn_position;
    3.16  val exn_messages = Runtime.exn_messages exn_position;
    3.17  val exn_message = Runtime.exn_message exn_position;
    3.18  

     4.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Jan 16 20:40:50 2013 +0100
     4.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Jan 16 20:41:29 2013 +0100
     4.3 @@ -22,6 +22,7 @@
     4.4      NONE => Position.none
     4.5    | SOME loc => position_of loc);
     4.6  
     4.7 +val exn_messages_ids = Runtime.exn_messages_ids exn_position;
     4.8  val exn_messages = Runtime.exn_messages exn_position;
     4.9  val exn_message = Runtime.exn_message exn_position;
    4.10  

     5.1 --- a/src/Pure/PIDE/command.ML	Wed Jan 16 20:40:50 2013 +0100
     5.2 +++ b/src/Pure/PIDE/command.ML	Wed Jan 16 20:41:29 2013 +0100
     5.3 @@ -64,15 +64,15 @@
     5.4  fun run int tr st =
     5.5    (case Toplevel.transition int tr st of
     5.6      SOME (st', NONE) => ([], SOME st')
     5.7 -  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
     5.8 -  | NONE => (ML_Compiler.exn_messages Runtime.TERMINATE, NONE));
     5.9 +  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
    5.10 +  | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
    5.11  
    5.12  fun check_cmts tr cmts st =
    5.13    Toplevel.setmp_thread_position tr
    5.14      (fn () => cmts
    5.15        |> maps (fn cmt =>
    5.16          (Thy_Output.check_text (Token.source_position_of cmt) st; [])
    5.17 -          handle exn => ML_Compiler.exn_messages exn)) ();
    5.18 +          handle exn => ML_Compiler.exn_messages_ids exn)) ();
    5.19  
    5.20  fun timing tr t =
    5.21    if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
    5.22 @@ -106,7 +106,7 @@
    5.23        val errs = errs1 @ errs2;
    5.24        val _ = timing tr (Timing.result start);
    5.25        val _ = Toplevel.status tr Markup.finished;
    5.26 -      val _ = List.app (Toplevel.error_msg tr) errs;
    5.27 +      val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
    5.28      in
    5.29        (case result of
    5.30          NONE =>

     6.1 --- a/src/Pure/PIDE/markup.ML	Wed Jan 16 20:40:50 2013 +0100
     6.2 +++ b/src/Pure/PIDE/markup.ML	Wed Jan 16 20:41:29 2013 +0100
     6.3 @@ -107,6 +107,7 @@
     6.4    val finishedN: string val finished: T
     6.5    val failedN: string val failed: T
     6.6    val serialN: string
     6.7 +  val exec_idN: string
     6.8    val initN: string
     6.9    val statusN: string
    6.10    val resultN: string
    6.11 @@ -364,6 +365,7 @@
    6.12  (* messages *)
    6.13  
    6.14  val serialN = "serial";
    6.15 +val exec_idN = "exec_id";
    6.16  
    6.17  val initN = "init";
    6.18  val statusN = "status";

     7.1 --- a/src/Pure/goal.ML	Wed Jan 16 20:40:50 2013 +0100
     7.2 +++ b/src/Pure/goal.ML	Wed Jan 16 20:41:29 2013 +0100
     7.3 @@ -137,8 +137,10 @@
     7.4  fun fork_name name e =
     7.5    uninterruptible (fn _ => fn () =>
     7.6      let
     7.7 -      val id = the_default 0 (Position.parse_id (Position.thread_data ()));
     7.8 +      val pos = Position.thread_data ();
     7.9 +      val id = the_default 0 (Position.parse_id pos);
    7.10        val _ = count_forked 1;
    7.11 +
    7.12        val future =
    7.13          (singleton o Future.forks)
    7.14            {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
    7.15 @@ -146,7 +148,9 @@
    7.16              let
    7.17                val task = the (Future.worker_task ());
    7.18                val _ = status task [Markup.running];
    7.19 -              val result = Exn.capture (Future.interruptible_task e) ();
    7.20 +              val result =
    7.21 +                Exn.capture (Future.interruptible_task e) ()
    7.22 +                |> Future.identify_result pos;
    7.23                val _ = status task [Markup.finished, Markup.joined];
    7.24                val _ =
    7.25                  (case result of
    7.26 @@ -156,7 +160,7 @@
    7.27                      else
    7.28                        (status task [Markup.failed];
    7.29                         Output.report (Markup.markup_only Markup.bad);
    7.30 -                       Output.error_msg (ML_Compiler.exn_message exn)));
    7.31 +                       List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
    7.32                val _ = count_forked ~1;
    7.33              in Exn.release result end);
    7.34        val _ = status (Future.task_of future) [Markup.forked];