--- a/Admin/polyml/future/ROOT.ML Wed Aug 17 15:03:30 2011 -0700
+++ b/Admin/polyml/future/ROOT.ML Wed Aug 17 15:12:34 2011 -0700
@@ -7,6 +7,22 @@
NONE => raise exn
| SOME location => PolyML.raiseWithLocation (exn, location));
+fun set_exn_serial i exn =
+ let
+ val (file, startLine, endLine) =
+ (case PolyML.exceptionLocation exn of
+ NONE => ("", 0, 0)
+ | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
+ val location =
+ {file = file, startLine = startLine, endLine = endLine,
+ startPosition = ~ i, endPosition = 0};
+ in PolyML.raiseWithLocation (exn, location) handle e => e end;
+
+fun get_exn_serial exn =
+ (case Option.map #startPosition (PolyML.exceptionLocation exn) of
+ NONE => NONE
+ | SOME i => if i >= 0 then NONE else SOME (~ i));
+
exception Interrupt = SML90.Interrupt;
val ord = SML90.ord;
val chr = SML90.chr;
@@ -61,6 +77,7 @@
use "General/alist.ML";
use "General/table.ML";
use "General/graph.ML";
+use "General/ord_list.ML";
structure Position =
struct
@@ -89,6 +106,7 @@
use "General/markup.ML";
use "Concurrent/single_assignment.ML";
use "Concurrent/time_limit.ML";
+use "Concurrent/par_exn.ML";
use "Concurrent/task_queue.ML";
use "Concurrent/future.ML";
use "Concurrent/lazy.ML";
--- a/src/Pure/Concurrent/future.ML Wed Aug 17 15:03:30 2011 -0700
+++ b/src/Pure/Concurrent/future.ML Wed Aug 17 15:12:34 2011 -0700
@@ -394,8 +394,12 @@
(* future jobs *)
-fun assign_result group result res =
+fun assign_result group result raw_res =
let
+ val res =
+ (case raw_res of
+ Exn.Exn exn => Exn.Exn (#2 (Par_Exn.serial exn))
+ | _ => raw_res);
val _ = Single_Assignment.assign result res
handle exn as Fail _ =>
(case Single_Assignment.peek result of
@@ -473,9 +477,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 15:12:34 2011 -0700
@@ -0,0 +1,63 @@
+(* 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 serial: exn -> serial * exn
+ val make: exn list -> exn
+ val dest: exn -> 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
+
+(* identification via serial numbers *)
+
+fun serial exn =
+ (case get_exn_serial exn of
+ SOME i => (i, exn)
+ | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
+
+val exn_ord = rev_order o int_ord o pairself (the o get_exn_serial);
+
+
+(* parallel exceptions *)
+
+exception Par_Exn of exn Ord_List.T;
+
+fun par_exns (Par_Exn exns) = SOME exns
+ | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [#2 (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 =
+ if all_res results then map Exn.release results
+ else
+ (case get_first
+ (fn res => if Exn.is_interrupt_exn res then NONE else Exn.get_exn res) results of
+ NONE => Exn.interrupt ()
+ | SOME exn => reraise exn);
+
+end;
+
--- a/src/Pure/Concurrent/par_list.ML Wed Aug 17 15:03:30 2011 -0700
+++ b/src/Pure/Concurrent/par_list.ML Wed Aug 17 15:12:34 2011 -0700
@@ -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 15:03:30 2011 -0700
+++ b/src/Pure/Concurrent/task_queue.ML Wed Aug 17 15:12:34 2011 -0700
@@ -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 15:03:30 2011 -0700
+++ b/src/Pure/General/exn.ML Wed Aug 17 15:12:34 2011 -0700
@@ -11,7 +11,6 @@
val get_exn: 'a result -> exn option
val capture: ('a -> 'b) -> 'a -> 'b result
val release: 'a result -> 'a
- val flat_result: 'a result result -> 'a result
val map_result: ('a -> 'b) -> 'a result -> 'b result
val maps_result: ('a -> 'b result) -> 'a result -> 'b result
exception Interrupt
@@ -21,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 =
@@ -47,13 +42,10 @@
fun release (Res y) = y
| release (Exn e) = reraise e;
-fun flat_result (Res x) = x
- | flat_result (Exn e) = Exn e;
-
fun map_result f (Res x) = Res (f x)
| map_result f (Exn e) = Exn e;
-fun maps_result f = flat_result o map_result f;
+fun maps_result f = (fn Res x => x | Exn e => Exn e) o map_result f;
(* interrupts *)
@@ -75,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 15:03:30 2011 -0700
+++ b/src/Pure/IsaMakefile Wed Aug 17 15:12:34 2011 -0700
@@ -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 15:03:30 2011 -0700
+++ b/src/Pure/Isar/runtime.ML Wed Aug 17 15:12:34 2011 -0700
@@ -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) exns
+ | 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/ML-Systems/polyml-5.2.1.ML Wed Aug 17 15:03:30 2011 -0700
+++ b/src/Pure/ML-Systems/polyml-5.2.1.ML Wed Aug 17 15:12:34 2011 -0700
@@ -13,6 +13,8 @@
end;
fun reraise exn = raise exn;
+fun set_exn_serial (_: int) (exn: exn) = exn;
+fun get_exn_serial (exn: exn) : int option = NONE;
use "ML-Systems/polyml_common.ML";
use "ML-Systems/multithreading_polyml.ML";
--- a/src/Pure/ML-Systems/polyml.ML Wed Aug 17 15:03:30 2011 -0700
+++ b/src/Pure/ML-Systems/polyml.ML Wed Aug 17 15:12:34 2011 -0700
@@ -17,6 +17,22 @@
NONE => raise exn
| SOME location => PolyML.raiseWithLocation (exn, location));
+fun set_exn_serial i exn =
+ let
+ val (file, startLine, endLine) =
+ (case PolyML.exceptionLocation exn of
+ NONE => ("", 0, 0)
+ | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
+ val location =
+ {file = file, startLine = startLine, endLine = endLine,
+ startPosition = ~ i, endPosition = 0};
+ in PolyML.raiseWithLocation (exn, location) handle e => e end;
+
+fun get_exn_serial exn =
+ (case Option.map #startPosition (PolyML.exceptionLocation exn) of
+ NONE => NONE
+ | SOME i => if i >= 0 then NONE else SOME (~ i));
+
use "ML-Systems/polyml_common.ML";
use "ML-Systems/multithreading_polyml.ML";
use "ML-Systems/unsynchronized.ML";
--- a/src/Pure/ML-Systems/smlnj.ML Wed Aug 17 15:03:30 2011 -0700
+++ b/src/Pure/ML-Systems/smlnj.ML Wed Aug 17 15:12:34 2011 -0700
@@ -3,10 +3,13 @@
Compatibility file for Standard ML of New Jersey 110 or later.
*)
+use "ML-Systems/proper_int.ML";
+
exception Interrupt;
fun reraise exn = raise exn;
+fun set_exn_serial (_: int) (exn: exn) = exn;
+fun get_exn_serial (exn: exn) : int option = NONE;
-use "ML-Systems/proper_int.ML";
use "ML-Systems/overloading_smlnj.ML";
use "General/exn.ML";
use "ML-Systems/single_assignment.ML";
--- a/src/Pure/PIDE/document.ML Wed Aug 17 15:03:30 2011 -0700
+++ b/src/Pure/PIDE/document.ML Wed Aug 17 15:12:34 2011 -0700
@@ -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 15:03:30 2011 -0700
+++ b/src/Pure/ROOT.ML Wed Aug 17 15:12:34 2011 -0700
@@ -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 15:03:30 2011 -0700
+++ b/src/Pure/Thy/thy_info.ML Wed Aug 17 15:12:34 2011 -0700
@@ -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 15:03:30 2011 -0700
+++ b/src/Pure/thm.ML Wed Aug 17 15:12:34 2011 -0700
@@ -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;