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

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Concurrent/par_exn.ML	Wed Aug 17 22:14:22 2011 +0200
     2.3 @@ -0,0 +1,49 @@
     2.4 +(*  Title:      Pure/Concurrent/par_exn.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Parallel exceptions as flattened results from acyclic graph of
     2.8 +evaluations.  Interrupt counts as neutral element.
     2.9 +*)
    2.10 +
    2.11 +signature PAR_EXN =
    2.12 +sig
    2.13 +  val make: exn list -> exn
    2.14 +  val dest: exn -> (serial * exn) list option
    2.15 +  val release_all: 'a Exn.result list -> 'a list
    2.16 +  val release_first: 'a Exn.result list -> 'a list
    2.17 +end;
    2.18 +
    2.19 +structure Par_Exn =
    2.20 +struct
    2.21 +
    2.22 +(* parallel exceptions *)
    2.23 +
    2.24 +exception Par_Exn of (serial * exn) Ord_List.T;
    2.25 +
    2.26 +fun exn_ord ((i, _), (j, _)) = int_ord (j, i);
    2.27 +
    2.28 +fun par_exns (Par_Exn exns) = SOME exns
    2.29 +  | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [(serial (), exn)];
    2.30 +
    2.31 +fun make exns =
    2.32 +  (case map_filter par_exns exns of
    2.33 +    [] => Exn.Interrupt
    2.34 +  | e :: es => Par_Exn (Library.foldl (Ord_List.merge exn_ord) (e, es)));
    2.35 +
    2.36 +fun dest (Par_Exn exns) = SOME (rev exns)
    2.37 +  | dest _ = NONE;
    2.38 +
    2.39 +
    2.40 +(* parallel results *)
    2.41 +
    2.42 +fun all_res results = forall (fn Exn.Res _ => true | _ => false) results;
    2.43 +
    2.44 +fun release_all results =
    2.45 +  if all_res results then map Exn.release results
    2.46 +  else raise make (map_filter Exn.get_exn results);
    2.47 +
    2.48 +fun release_first results = release_all results
    2.49 +  handle Par_Exn ((serial, exn) :: _) => reraise exn;  (* FIXME preserve serial in location (?!?) *)
    2.50 +
    2.51 +end;
    2.52 +

     3.1 --- a/src/Pure/Concurrent/par_list.ML	Wed Aug 17 20:08:36 2011 +0200
     3.2 +++ b/src/Pure/Concurrent/par_list.ML	Wed Aug 17 22:14:22 2011 +0200
     3.3 @@ -41,7 +41,7 @@
     3.4          handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
     3.5      in results end;
     3.6  
     3.7 -fun map_name name f xs = Exn.release_first (managed_results name f xs);
     3.8 +fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
     3.9  fun map f = map_name "Par_List.map" f;
    3.10  
    3.11  fun get_some f xs =
    3.12 @@ -55,7 +55,7 @@
    3.13    in
    3.14      (case get_first found results of
    3.15        SOME y => SOME y
    3.16 -    | NONE => (Exn.release_first results; NONE))
    3.17 +    | NONE => (Par_Exn.release_first results; NONE))
    3.18    end;
    3.19  
    3.20  fun find_some P = get_some (fn x => if P x then SOME x else NONE);

     4.1 --- a/src/Pure/Concurrent/task_queue.ML	Wed Aug 17 20:08:36 2011 +0200
     4.2 +++ b/src/Pure/Concurrent/task_queue.ML	Wed Aug 17 22:14:22 2011 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4    val eq_group: group * group -> bool
     4.5    val cancel_group: group -> exn -> unit
     4.6    val is_canceled: group -> bool
     4.7 -  val group_status: group -> exn list
     4.8 +  val group_status: group -> exn option
     4.9    val str_of_group: group -> string
    4.10    val str_of_groups: group -> string
    4.11    type task
    4.12 @@ -56,12 +56,12 @@
    4.13  abstype group = Group of
    4.14   {parent: group option,
    4.15    id: int,
    4.16 -  status: exn list Synchronized.var}
    4.17 +  status: exn option Synchronized.var}
    4.18  with
    4.19  
    4.20  fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
    4.21  
    4.22 -fun new_group parent = make_group (parent, new_id (), Synchronized.var "group" []);
    4.23 +fun new_group parent = make_group (parent, new_id (), Synchronized.var "group_status" NONE);
    4.24  
    4.25  fun group_id (Group {id, ...}) = id;
    4.26  fun eq_group (group1, group2) = group_id group1 = group_id group2;
    4.27 @@ -74,17 +74,20 @@
    4.28  
    4.29  fun cancel_group (Group {status, ...}) exn =
    4.30    Synchronized.change status
    4.31 -    (fn exns =>
    4.32 -      if not (Exn.is_interrupt exn) orelse null exns then exn :: exns
    4.33 -      else exns);
    4.34 +    (fn exns => SOME (Par_Exn.make (exn :: the_list exns)));
    4.35  
    4.36  fun is_canceled (Group {parent, status, ...}) =
    4.37 -  not (null (Synchronized.value status)) orelse
    4.38 +  is_some (Synchronized.value status) orelse
    4.39      (case parent of NONE => false | SOME group => is_canceled group);
    4.40  
    4.41 -fun group_status (Group {parent, status, ...}) =
    4.42 -  Synchronized.value status @
    4.43 -    (case parent of NONE => [] | SOME group => group_status group);
    4.44 +fun group_exns (Group {parent, status, ...}) =
    4.45 +  the_list (Synchronized.value status) @
    4.46 +    (case parent of NONE => [] | SOME group => group_exns group);
    4.47 +
    4.48 +fun group_status group =
    4.49 +  (case group_exns group of
    4.50 +    [] => NONE
    4.51 +  | exns => SOME (Par_Exn.make exns));
    4.52  
    4.53  fun str_of_group group =
    4.54    (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));

     5.1 --- a/src/Pure/General/exn.ML	Wed Aug 17 20:08:36 2011 +0200
     5.2 +++ b/src/Pure/General/exn.ML	Wed Aug 17 22:14:22 2011 +0200
     5.3 @@ -20,10 +20,6 @@
     5.4    val is_interrupt_exn: 'a result -> bool
     5.5    val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
     5.6    exception EXCEPTIONS of exn list
     5.7 -  val flatten: exn -> exn list
     5.8 -  val flatten_list: exn list -> exn list
     5.9 -  val release_all: 'a result list -> 'a list
    5.10 -  val release_first: 'a result list -> 'a list
    5.11  end;
    5.12  
    5.13  structure Exn: EXN =
    5.14 @@ -71,23 +67,10 @@
    5.15    Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
    5.16  
    5.17  
    5.18 -(* nested exceptions *)
    5.19 +(* concatenated exceptions *)
    5.20  
    5.21  exception EXCEPTIONS of exn list;
    5.22  
    5.23 -fun flatten (EXCEPTIONS exns) = flatten_list exns
    5.24 -  | flatten exn = if is_interrupt exn then [] else [exn]
    5.25 -and flatten_list exns = List.concat (map flatten exns);
    5.26 -
    5.27 -fun release_all results =
    5.28 -  if List.all (fn Res _ => true | _ => false) results
    5.29 -  then map (fn Res x => x) results
    5.30 -  else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
    5.31 -
    5.32 -fun release_first results = release_all results
    5.33 -  handle EXCEPTIONS [] => interrupt ()
    5.34 -    | EXCEPTIONS (exn :: _) => reraise exn;
    5.35 -
    5.36  end;
    5.37  
    5.38  datatype illegal = Interrupt;

     6.1 --- a/src/Pure/IsaMakefile	Wed Aug 17 20:08:36 2011 +0200
     6.2 +++ b/src/Pure/IsaMakefile	Wed Aug 17 22:14:22 2011 +0200
     6.3 @@ -60,6 +60,7 @@
     6.4    Concurrent/lazy.ML					\
     6.5    Concurrent/lazy_sequential.ML				\
     6.6    Concurrent/mailbox.ML					\
     6.7 +  Concurrent/par_exn.ML					\
     6.8    Concurrent/par_list.ML				\
     6.9    Concurrent/par_list_sequential.ML			\
    6.10    Concurrent/simple_thread.ML				\

     7.1 --- a/src/Pure/Isar/runtime.ML	Wed Aug 17 20:08:36 2011 +0200
     7.2 +++ b/src/Pure/Isar/runtime.ML	Wed Aug 17 22:14:22 2011 +0200
     7.3 @@ -60,34 +60,38 @@
     7.4      fun exn_msgs context exn =
     7.5        if Exn.is_interrupt exn then []
     7.6        else
     7.7 -        (case exn of
     7.8 -          Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
     7.9 -        | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
    7.10 -        | EXCURSION_FAIL (exn, loc) =>
    7.11 -            map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)) (exn_msgs context exn)
    7.12 -        | TERMINATE => ["Exit"]
    7.13 -        | TimeLimit.TimeOut => ["Timeout"]
    7.14 -        | TOPLEVEL_ERROR => ["Error"]
    7.15 -        | ERROR msg => [msg]
    7.16 -        | Fail msg => [raised exn "Fail" [msg]]
    7.17 -        | THEORY (msg, thys) =>
    7.18 -            [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
    7.19 -        | Ast.AST (msg, asts) =>
    7.20 -            [raised exn "AST" (msg ::
    7.21 -              (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
    7.22 -        | TYPE (msg, Ts, ts) =>
    7.23 -            [raised exn "TYPE" (msg ::
    7.24 -              (if detailed then
    7.25 -                if_context context Syntax.string_of_typ Ts @
    7.26 -                if_context context Syntax.string_of_term ts
    7.27 -               else []))]
    7.28 -        | TERM (msg, ts) =>
    7.29 -            [raised exn "TERM" (msg ::
    7.30 -              (if detailed then if_context context Syntax.string_of_term ts else []))]
    7.31 -        | THM (msg, i, thms) =>
    7.32 -            [raised exn ("THM " ^ string_of_int i) (msg ::
    7.33 -              (if detailed then if_context context Display.string_of_thm thms else []))]
    7.34 -        | _ => [raised exn (General.exnMessage exn) []]);
    7.35 +        (case Par_Exn.dest exn of
    7.36 +          SOME exns => maps (exn_msgs context o #2) exns   (* FIXME include serial in message!? *)
    7.37 +        | NONE =>
    7.38 +            (case exn of
    7.39 +              Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
    7.40 +            | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
    7.41 +            | EXCURSION_FAIL (exn, loc) =>
    7.42 +                map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc))
    7.43 +                  (exn_msgs context exn)
    7.44 +            | TERMINATE => ["Exit"]
    7.45 +            | TimeLimit.TimeOut => ["Timeout"]
    7.46 +            | TOPLEVEL_ERROR => ["Error"]
    7.47 +            | ERROR msg => [msg]
    7.48 +            | Fail msg => [raised exn "Fail" [msg]]
    7.49 +            | THEORY (msg, thys) =>
    7.50 +                [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
    7.51 +            | Ast.AST (msg, asts) =>
    7.52 +                [raised exn "AST" (msg ::
    7.53 +                  (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
    7.54 +            | TYPE (msg, Ts, ts) =>
    7.55 +                [raised exn "TYPE" (msg ::
    7.56 +                  (if detailed then
    7.57 +                    if_context context Syntax.string_of_typ Ts @
    7.58 +                    if_context context Syntax.string_of_term ts
    7.59 +                   else []))]
    7.60 +            | TERM (msg, ts) =>
    7.61 +                [raised exn "TERM" (msg ::
    7.62 +                  (if detailed then if_context context Syntax.string_of_term ts else []))]
    7.63 +            | THM (msg, i, thms) =>
    7.64 +                [raised exn ("THM " ^ string_of_int i) (msg ::
    7.65 +                  (if detailed then if_context context Display.string_of_thm thms else []))]
    7.66 +            | _ => [raised exn (General.exnMessage exn) []]));
    7.67    in exn_msgs NONE e end;
    7.68  
    7.69  fun exn_message exn_position exn =

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

     9.1 --- a/src/Pure/ROOT.ML	Wed Aug 17 20:08:36 2011 +0200
     9.2 +++ b/src/Pure/ROOT.ML	Wed Aug 17 22:14:22 2011 +0200
     9.3 @@ -77,7 +77,7 @@
     9.4  then use "Concurrent/bash.ML"
     9.5  else use "Concurrent/bash_sequential.ML";
     9.6  
     9.7 -use "Concurrent/mailbox.ML";
     9.8 +use "Concurrent/par_exn.ML";
     9.9  use "Concurrent/task_queue.ML";
    9.10  use "Concurrent/future.ML";
    9.11  
    9.12 @@ -89,6 +89,7 @@
    9.13  if Multithreading.available then ()
    9.14  else use "Concurrent/par_list_sequential.ML";
    9.15  
    9.16 +use "Concurrent/mailbox.ML";
    9.17  use "Concurrent/cache.ML";
    9.18  
    9.19  

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

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