identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;

--- 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

--- a/src/Pure/Isar/runtime.ML	Wed Jan 16 20:40:50 2013 +0100
+++ b/src/Pure/Isar/runtime.ML	Wed Jan 16 20:41:29 2013 +0100
@@ -12,6 +12,7 @@
   exception TOPLEVEL_ERROR
   val debug: bool Unsynchronized.ref
   val exn_context: Proof.context option -> exn -> exn
+  val exn_messages_ids: (exn -> Position.T) -> exn -> ((serial * string) * string option) list
   val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
   val exn_message: (exn -> Position.T) -> exn -> string
   val debugging: ('a -> 'b) -> 'a -> 'b
@@ -42,22 +43,28 @@
 
 (* exn_message *)
 
+local
+
 fun if_context NONE _ _ = []
   | if_context (SOME ctxt) f xs = map (f ctxt) xs;
 
-fun exn_messages exn_position e =
+fun identify exn =
   let
-    fun identify exn =
-      let val exn' = Par_Exn.identify [] exn
-      in (Par_Exn.the_serial exn', exn') end;
+    val exn' = Par_Exn.identify [] exn;
+    val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
+  in ((Par_Exn.the_serial exn', exn'), exec_id) end;
 
-    fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
-      | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
-      | flatten context exn =
-          (case Par_Exn.dest exn of
-            SOME exns => maps (flatten context) exns
-          | NONE => [(context, identify exn)]);
+fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
+  | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
+  | flatten context exn =
+      (case Par_Exn.dest exn of
+        SOME exns => maps (flatten context) exns
+      | NONE => [(context, identify exn)]);
 
+in
+
+fun exn_messages_ids exn_position e =
+  let
     fun raised exn name msgs =
       let val pos = Position.here (exn_position exn) in
         (case msgs of
@@ -66,10 +73,10 @@
         | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
       end;
 
-    fun exn_msgs (context, (i, exn)) =
+    fun exn_msgs (context, ((i, exn), id)) =
       (case exn of
         EXCURSION_FAIL (exn, loc) =>
-          map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
+          map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id))
             (sorted_msgs context exn)
       | _ =>
         let
@@ -94,12 +101,17 @@
                 raised exn ("THM " ^ string_of_int i)
                   (msg :: if_context context Display.string_of_thm thms)
             | _ => raised exn (General.exnMessage exn) []);
-        in [(i, msg)] end)
+        in [((i, msg), id)] end)
       and sorted_msgs context exn =
-        sort_distinct (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
+        sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
 
   in sorted_msgs NONE e end;
 
+end;
+
+fun exn_messages exn_position exn =
+  map #1 (exn_messages_ids exn_position exn);
+
 fun exn_message exn_position exn =
   (case exn_messages exn_position exn of
     [] => "Interrupt"

--- a/src/Pure/ML/ml_compiler.ML	Wed Jan 16 20:40:50 2013 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Wed Jan 16 20:41:29 2013 +0100
@@ -7,6 +7,7 @@
 signature ML_COMPILER =
 sig
   val exn_position: exn -> Position.T
+  val exn_messages_ids: exn -> ((serial * string) * string option) list
   val exn_messages: exn -> (serial * string) list
   val exn_message: exn -> string
   val eval: bool -> Position.T -> ML_Lex.token list -> unit
@@ -16,6 +17,7 @@
 struct
 
 fun exn_position _ = Position.none;
+val exn_messages_ids = Runtime.exn_messages_ids exn_position;
 val exn_messages = Runtime.exn_messages exn_position;
 val exn_message = Runtime.exn_message exn_position;
 

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

--- a/src/Pure/PIDE/command.ML	Wed Jan 16 20:40:50 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Jan 16 20:41:29 2013 +0100
@@ -64,15 +64,15 @@
 fun run int tr st =
   (case Toplevel.transition int tr st of
     SOME (st', NONE) => ([], SOME st')
-  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
-  | NONE => (ML_Compiler.exn_messages Runtime.TERMINATE, NONE));
+  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
+  | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
 
 fun check_cmts tr cmts st =
   Toplevel.setmp_thread_position tr
     (fn () => cmts
       |> maps (fn cmt =>
         (Thy_Output.check_text (Token.source_position_of cmt) st; [])
-          handle exn => ML_Compiler.exn_messages exn)) ();
+          handle exn => ML_Compiler.exn_messages_ids exn)) ();
 
 fun timing tr t =
   if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
@@ -106,7 +106,7 @@
       val errs = errs1 @ errs2;
       val _ = timing tr (Timing.result start);
       val _ = Toplevel.status tr Markup.finished;
-      val _ = List.app (Toplevel.error_msg tr) errs;
+      val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
     in
       (case result of
         NONE =>

--- a/src/Pure/PIDE/markup.ML	Wed Jan 16 20:40:50 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Jan 16 20:41:29 2013 +0100
@@ -107,6 +107,7 @@
   val finishedN: string val finished: T
   val failedN: string val failed: T
   val serialN: string
+  val exec_idN: string
   val initN: string
   val statusN: string
   val resultN: string
@@ -364,6 +365,7 @@
 (* messages *)
 
 val serialN = "serial";
+val exec_idN = "exec_id";
 
 val initN = "init";
 val statusN = "status";

--- a/src/Pure/goal.ML	Wed Jan 16 20:40:50 2013 +0100
+++ b/src/Pure/goal.ML	Wed Jan 16 20:41:29 2013 +0100
@@ -137,8 +137,10 @@
 fun fork_name name e =
   uninterruptible (fn _ => fn () =>
     let
-      val id = the_default 0 (Position.parse_id (Position.thread_data ()));
+      val pos = Position.thread_data ();
+      val id = the_default 0 (Position.parse_id pos);
       val _ = count_forked 1;
+
       val future =
         (singleton o Future.forks)
           {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
@@ -146,7 +148,9 @@
             let
               val task = the (Future.worker_task ());
               val _ = status task [Markup.running];
-              val result = Exn.capture (Future.interruptible_task e) ();
+              val result =
+                Exn.capture (Future.interruptible_task e) ()
+                |> Future.identify_result pos;
               val _ = status task [Markup.finished, Markup.joined];
               val _ =
                 (case result of
@@ -156,7 +160,7 @@
                     else
                       (status task [Markup.failed];
                        Output.report (Markup.markup_only Markup.bad);
-                       Output.error_msg (ML_Compiler.exn_message exn)));
+                       List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
               val _ = count_forked ~1;
             in Exn.release result end);
       val _ = status (Future.task_of future) [Markup.forked];