more systematic handling of parallel exceptions;
distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;

--- a/src/Pure/Concurrent/future.ML	Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Aug 17 22:14:22 2011 +0200
@@ -473,9 +473,9 @@
     NONE => Exn.Exn (Fail "Unfinished future")
   | SOME res =>
       if Exn.is_interrupt_exn res then
-        (case Exn.flatten_list (Task_Queue.group_status (Task_Queue.group_of_task (task_of x))) of
-          [] => res
-        | exns => Exn.Exn (Exn.EXCEPTIONS exns))
+        (case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of
+          NONE => res
+        | SOME exn => Exn.Exn exn)
       else res);
 
 fun join_next deps = (*requires SYNCHRONIZED*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/par_exn.ML	Wed Aug 17 22:14:22 2011 +0200
@@ -0,0 +1,49 @@
+(*  Title:      Pure/Concurrent/par_exn.ML
+    Author:     Makarius
+
+Parallel exceptions as flattened results from acyclic graph of
+evaluations.  Interrupt counts as neutral element.
+*)
+
+signature PAR_EXN =
+sig
+  val make: exn list -> exn
+  val dest: exn -> (serial * exn) list option
+  val release_all: 'a Exn.result list -> 'a list
+  val release_first: 'a Exn.result list -> 'a list
+end;
+
+structure Par_Exn =
+struct
+
+(* parallel exceptions *)
+
+exception Par_Exn of (serial * exn) Ord_List.T;
+
+fun exn_ord ((i, _), (j, _)) = int_ord (j, i);
+
+fun par_exns (Par_Exn exns) = SOME exns
+  | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [(serial (), exn)];
+
+fun make exns =
+  (case map_filter par_exns exns of
+    [] => Exn.Interrupt
+  | e :: es => Par_Exn (Library.foldl (Ord_List.merge exn_ord) (e, es)));
+
+fun dest (Par_Exn exns) = SOME (rev exns)
+  | dest _ = NONE;
+
+
+(* parallel results *)
+
+fun all_res results = forall (fn Exn.Res _ => true | _ => false) results;
+
+fun release_all results =
+  if all_res results then map Exn.release results
+  else raise make (map_filter Exn.get_exn results);
+
+fun release_first results = release_all results
+  handle Par_Exn ((serial, exn) :: _) => reraise exn;  (* FIXME preserve serial in location (?!?) *)
+
+end;
+

--- a/src/Pure/Concurrent/par_list.ML	Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Wed Aug 17 22:14:22 2011 +0200
@@ -41,7 +41,7 @@
         handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
     in results end;
 
-fun map_name name f xs = Exn.release_first (managed_results name f xs);
+fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
 fun map f = map_name "Par_List.map" f;
 
 fun get_some f xs =
@@ -55,7 +55,7 @@
   in
     (case get_first found results of
       SOME y => SOME y
-    | NONE => (Exn.release_first results; NONE))
+    | NONE => (Par_Exn.release_first results; NONE))
   end;
 
 fun find_some P = get_some (fn x => if P x then SOME x else NONE);

--- a/src/Pure/Concurrent/task_queue.ML	Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Aug 17 22:14:22 2011 +0200
@@ -12,7 +12,7 @@
   val eq_group: group * group -> bool
   val cancel_group: group -> exn -> unit
   val is_canceled: group -> bool
-  val group_status: group -> exn list
+  val group_status: group -> exn option
   val str_of_group: group -> string
   val str_of_groups: group -> string
   type task
@@ -56,12 +56,12 @@
 abstype group = Group of
  {parent: group option,
   id: int,
-  status: exn list Synchronized.var}
+  status: exn option Synchronized.var}
 with
 
 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
 
-fun new_group parent = make_group (parent, new_id (), Synchronized.var "group" []);
+fun new_group parent = make_group (parent, new_id (), Synchronized.var "group_status" NONE);
 
 fun group_id (Group {id, ...}) = id;
 fun eq_group (group1, group2) = group_id group1 = group_id group2;
@@ -74,17 +74,20 @@
 
 fun cancel_group (Group {status, ...}) exn =
   Synchronized.change status
-    (fn exns =>
-      if not (Exn.is_interrupt exn) orelse null exns then exn :: exns
-      else exns);
+    (fn exns => SOME (Par_Exn.make (exn :: the_list exns)));
 
 fun is_canceled (Group {parent, status, ...}) =
-  not (null (Synchronized.value status)) orelse
+  is_some (Synchronized.value status) orelse
     (case parent of NONE => false | SOME group => is_canceled group);
 
-fun group_status (Group {parent, status, ...}) =
-  Synchronized.value status @
-    (case parent of NONE => [] | SOME group => group_status group);
+fun group_exns (Group {parent, status, ...}) =
+  the_list (Synchronized.value status) @
+    (case parent of NONE => [] | SOME group => group_exns group);
+
+fun group_status group =
+  (case group_exns group of
+    [] => NONE
+  | exns => SOME (Par_Exn.make exns));
 
 fun str_of_group group =
   (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));

--- a/src/Pure/General/exn.ML	Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/General/exn.ML	Wed Aug 17 22:14:22 2011 +0200
@@ -20,10 +20,6 @@
   val is_interrupt_exn: 'a result -> bool
   val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
   exception EXCEPTIONS of exn list
-  val flatten: exn -> exn list
-  val flatten_list: exn list -> exn list
-  val release_all: 'a result list -> 'a list
-  val release_first: 'a result list -> 'a list
 end;
 
 structure Exn: EXN =
@@ -71,23 +67,10 @@
   Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
 
 
-(* nested exceptions *)
+(* concatenated exceptions *)
 
 exception EXCEPTIONS of exn list;
 
-fun flatten (EXCEPTIONS exns) = flatten_list exns
-  | flatten exn = if is_interrupt exn then [] else [exn]
-and flatten_list exns = List.concat (map flatten exns);
-
-fun release_all results =
-  if List.all (fn Res _ => true | _ => false) results
-  then map (fn Res x => x) results
-  else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
-
-fun release_first results = release_all results
-  handle EXCEPTIONS [] => interrupt ()
-    | EXCEPTIONS (exn :: _) => reraise exn;
-
 end;
 
 datatype illegal = Interrupt;

--- a/src/Pure/IsaMakefile	Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/IsaMakefile	Wed Aug 17 22:14:22 2011 +0200
@@ -60,6 +60,7 @@
   Concurrent/lazy.ML					\
   Concurrent/lazy_sequential.ML				\
   Concurrent/mailbox.ML					\
+  Concurrent/par_exn.ML					\
   Concurrent/par_list.ML				\
   Concurrent/par_list_sequential.ML			\
   Concurrent/simple_thread.ML				\

--- a/src/Pure/Isar/runtime.ML	Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/Isar/runtime.ML	Wed Aug 17 22:14:22 2011 +0200
@@ -60,34 +60,38 @@
     fun exn_msgs context exn =
       if Exn.is_interrupt exn then []
       else
-        (case exn of
-          Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
-        | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
-        | EXCURSION_FAIL (exn, loc) =>
-            map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)) (exn_msgs context exn)
-        | TERMINATE => ["Exit"]
-        | TimeLimit.TimeOut => ["Timeout"]
-        | TOPLEVEL_ERROR => ["Error"]
-        | ERROR msg => [msg]
-        | Fail msg => [raised exn "Fail" [msg]]
-        | THEORY (msg, thys) =>
-            [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
-        | Ast.AST (msg, asts) =>
-            [raised exn "AST" (msg ::
-              (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
-        | TYPE (msg, Ts, ts) =>
-            [raised exn "TYPE" (msg ::
-              (if detailed then
-                if_context context Syntax.string_of_typ Ts @
-                if_context context Syntax.string_of_term ts
-               else []))]
-        | TERM (msg, ts) =>
-            [raised exn "TERM" (msg ::
-              (if detailed then if_context context Syntax.string_of_term ts else []))]
-        | THM (msg, i, thms) =>
-            [raised exn ("THM " ^ string_of_int i) (msg ::
-              (if detailed then if_context context Display.string_of_thm thms else []))]
-        | _ => [raised exn (General.exnMessage exn) []]);
+        (case Par_Exn.dest exn of
+          SOME exns => maps (exn_msgs context o #2) exns   (* FIXME include serial in message!? *)
+        | NONE =>
+            (case exn of
+              Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
+            | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
+            | EXCURSION_FAIL (exn, loc) =>
+                map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc))
+                  (exn_msgs context exn)
+            | TERMINATE => ["Exit"]
+            | TimeLimit.TimeOut => ["Timeout"]
+            | TOPLEVEL_ERROR => ["Error"]
+            | ERROR msg => [msg]
+            | Fail msg => [raised exn "Fail" [msg]]
+            | THEORY (msg, thys) =>
+                [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
+            | Ast.AST (msg, asts) =>
+                [raised exn "AST" (msg ::
+                  (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
+            | TYPE (msg, Ts, ts) =>
+                [raised exn "TYPE" (msg ::
+                  (if detailed then
+                    if_context context Syntax.string_of_typ Ts @
+                    if_context context Syntax.string_of_term ts
+                   else []))]
+            | TERM (msg, ts) =>
+                [raised exn "TERM" (msg ::
+                  (if detailed then if_context context Syntax.string_of_term ts else []))]
+            | THM (msg, i, thms) =>
+                [raised exn ("THM " ^ string_of_int i) (msg ::
+                  (if detailed then if_context context Display.string_of_thm thms else []))]
+            | _ => [raised exn (General.exnMessage exn) []]));
   in exn_msgs NONE e end;
 
 fun exn_message exn_position exn =

--- a/src/Pure/PIDE/document.ML	Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Aug 17 22:14:22 2011 +0200
@@ -372,7 +372,7 @@
                         |> set_result result;
                     in ((assigns, execs, [(name, node')]), node') end)
               end))
-      |> Future.join_results |> Exn.release_all |> map #1;
+      |> Future.join_results |> Par_Exn.release_all |> map #1;
 
     val state' = state
       |> fold (fold define_exec o #2) updates

--- a/src/Pure/ROOT.ML	Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/ROOT.ML	Wed Aug 17 22:14:22 2011 +0200
@@ -77,7 +77,7 @@
 then use "Concurrent/bash.ML"
 else use "Concurrent/bash_sequential.ML";
 
-use "Concurrent/mailbox.ML";
+use "Concurrent/par_exn.ML";
 use "Concurrent/task_queue.ML";
 use "Concurrent/future.ML";
 
@@ -89,6 +89,7 @@
 if Multithreading.available then ()
 else use "Concurrent/par_list_sequential.ML";
 
+use "Concurrent/mailbox.ML";
 use "Concurrent/cache.ML";
 
 

--- a/src/Pure/Thy/thy_info.ML	Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Aug 17 22:14:22 2011 +0200
@@ -207,7 +207,7 @@
                   " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
     | Finished thy => Future.value (thy, Future.value (), I)))
   #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn])
-  #> rev #> Exn.release_all) #> ignore;
+  #> rev #> Par_Exn.release_all) #> ignore;
 
 in
 

--- a/src/Pure/thm.ML	Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/thm.ML	Wed Aug 17 22:14:22 2011 +0200
@@ -515,7 +515,7 @@
 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
   Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
     (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
-and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
+and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
 
 val join_proofs = Proofterm.join_bodies o map fulfill_body;