1.1 --- a/src/Pure/Concurrent/future.ML Wed Aug 17 14:32:48 2011 -0700
1.2 +++ b/src/Pure/Concurrent/future.ML Wed Aug 17 23:41:47 2011 +0200
1.3 @@ -394,8 +394,12 @@
1.4
1.5 (* future jobs *)
1.6
1.7 -fun assign_result group result res =
1.8 +fun assign_result group result raw_res =
1.9 let
1.10 + val res =
1.11 + (case raw_res of
1.12 + Exn.Exn exn => Exn.Exn (#2 (Par_Exn.serial exn))
1.13 + | _ => raw_res);
1.14 val _ = Single_Assignment.assign result res
1.15 handle exn as Fail _ =>
1.16 (case Single_Assignment.peek result of
1.17 @@ -473,9 +477,9 @@
1.18 NONE => Exn.Exn (Fail "Unfinished future")
1.19 | SOME res =>
1.20 if Exn.is_interrupt_exn res then
1.21 - (case Exn.flatten_list (Task_Queue.group_status (Task_Queue.group_of_task (task_of x))) of
1.22 - [] => res
1.23 - | exns => Exn.Exn (Exn.EXCEPTIONS exns))
1.24 + (case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of
1.25 + NONE => res
1.26 + | SOME exn => Exn.Exn exn)
1.27 else res);
1.28
1.29 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 23:41:47 2011 +0200
2.3 @@ -0,0 +1,63 @@
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 serial: exn -> serial * exn
2.14 + val make: exn list -> exn
2.15 + val dest: exn -> exn list option
2.16 + val release_all: 'a Exn.result list -> 'a list
2.17 + val release_first: 'a Exn.result list -> 'a list
2.18 +end;
2.19 +
2.20 +structure Par_Exn =
2.21 +struct
2.22 +
2.23 +(* identification via serial numbers *)
2.24 +
2.25 +fun serial exn =
2.26 + (case get_exn_serial exn of
2.27 + SOME i => (i, exn)
2.28 + | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
2.29 +
2.30 +val exn_ord = rev_order o int_ord o pairself (the o get_exn_serial);
2.31 +
2.32 +
2.33 +(* parallel exceptions *)
2.34 +
2.35 +exception Par_Exn of exn Ord_List.T;
2.36 +
2.37 +fun par_exns (Par_Exn exns) = SOME exns
2.38 + | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [#2 (serial exn)];
2.39 +
2.40 +fun make exns =
2.41 + (case map_filter par_exns exns of
2.42 + [] => Exn.Interrupt
2.43 + | e :: es => Par_Exn (Library.foldl (Ord_List.merge exn_ord) (e, es)));
2.44 +
2.45 +fun dest (Par_Exn exns) = SOME (rev exns)
2.46 + | dest _ = NONE;
2.47 +
2.48 +
2.49 +(* parallel results *)
2.50 +
2.51 +fun all_res results = forall (fn Exn.Res _ => true | _ => false) results;
2.52 +
2.53 +fun release_all results =
2.54 + if all_res results then map Exn.release results
2.55 + else raise make (map_filter Exn.get_exn results);
2.56 +
2.57 +fun release_first results =
2.58 + if all_res results then map Exn.release results
2.59 + else
2.60 + (case get_first
2.61 + (fn res => if Exn.is_interrupt_exn res then NONE else Exn.get_exn res) results of
2.62 + NONE => Exn.interrupt ()
2.63 + | SOME exn => reraise exn);
2.64 +
2.65 +end;
2.66 +
3.1 --- a/src/Pure/Concurrent/par_list.ML Wed Aug 17 14:32:48 2011 -0700
3.2 +++ b/src/Pure/Concurrent/par_list.ML Wed Aug 17 23:41:47 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 14:32:48 2011 -0700
4.2 +++ b/src/Pure/Concurrent/task_queue.ML Wed Aug 17 23:41:47 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 14:32:48 2011 -0700
5.2 +++ b/src/Pure/General/exn.ML Wed Aug 17 23:41:47 2011 +0200
5.3 @@ -11,7 +11,6 @@
5.4 val get_exn: 'a result -> exn option
5.5 val capture: ('a -> 'b) -> 'a -> 'b result
5.6 val release: 'a result -> 'a
5.7 - val flat_result: 'a result result -> 'a result
5.8 val map_result: ('a -> 'b) -> 'a result -> 'b result
5.9 val maps_result: ('a -> 'b result) -> 'a result -> 'b result
5.10 exception Interrupt
5.11 @@ -21,10 +20,6 @@
5.12 val is_interrupt_exn: 'a result -> bool
5.13 val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
5.14 exception EXCEPTIONS of exn list
5.15 - val flatten: exn -> exn list
5.16 - val flatten_list: exn list -> exn list
5.17 - val release_all: 'a result list -> 'a list
5.18 - val release_first: 'a result list -> 'a list
5.19 end;
5.20
5.21 structure Exn: EXN =
5.22 @@ -47,13 +42,10 @@
5.23 fun release (Res y) = y
5.24 | release (Exn e) = reraise e;
5.25
5.26 -fun flat_result (Res x) = x
5.27 - | flat_result (Exn e) = Exn e;
5.28 -
5.29 fun map_result f (Res x) = Res (f x)
5.30 | map_result f (Exn e) = Exn e;
5.31
5.32 -fun maps_result f = flat_result o map_result f;
5.33 +fun maps_result f = (fn Res x => x | Exn e => Exn e) o map_result f;
5.34
5.35
5.36 (* interrupts *)
5.37 @@ -75,23 +67,10 @@
5.38 Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
5.39
5.40
5.41 -(* nested exceptions *)
5.42 +(* concatenated exceptions *)
5.43
5.44 exception EXCEPTIONS of exn list;
5.45
5.46 -fun flatten (EXCEPTIONS exns) = flatten_list exns
5.47 - | flatten exn = if is_interrupt exn then [] else [exn]
5.48 -and flatten_list exns = List.concat (map flatten exns);
5.49 -
5.50 -fun release_all results =
5.51 - if List.all (fn Res _ => true | _ => false) results
5.52 - then map (fn Res x => x) results
5.53 - else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
5.54 -
5.55 -fun release_first results = release_all results
5.56 - handle EXCEPTIONS [] => interrupt ()
5.57 - | EXCEPTIONS (exn :: _) => reraise exn;
5.58 -
5.59 end;
5.60
5.61 datatype illegal = Interrupt;
6.1 --- a/src/Pure/IsaMakefile Wed Aug 17 14:32:48 2011 -0700
6.2 +++ b/src/Pure/IsaMakefile Wed Aug 17 23:41:47 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 14:32:48 2011 -0700
7.2 +++ b/src/Pure/Isar/runtime.ML Wed Aug 17 23:41:47 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) exns
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/ML-Systems/polyml-5.2.1.ML Wed Aug 17 14:32:48 2011 -0700
8.2 +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML Wed Aug 17 23:41:47 2011 +0200
8.3 @@ -13,6 +13,8 @@
8.4 end;
8.5
8.6 fun reraise exn = raise exn;
8.7 +fun set_exn_serial (_: int) (exn: exn) = exn;
8.8 +fun get_exn_serial (exn: exn) : int option = NONE;
8.9
8.10 use "ML-Systems/polyml_common.ML";
8.11 use "ML-Systems/multithreading_polyml.ML";
9.1 --- a/src/Pure/ML-Systems/polyml.ML Wed Aug 17 14:32:48 2011 -0700
9.2 +++ b/src/Pure/ML-Systems/polyml.ML Wed Aug 17 23:41:47 2011 +0200
9.3 @@ -17,6 +17,22 @@
9.4 NONE => raise exn
9.5 | SOME location => PolyML.raiseWithLocation (exn, location));
9.6
9.7 +fun set_exn_serial i exn =
9.8 + let
9.9 + val (file, startLine, endLine) =
9.10 + (case PolyML.exceptionLocation exn of
9.11 + NONE => ("", 0, 0)
9.12 + | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
9.13 + val location =
9.14 + {file = file, startLine = startLine, endLine = endLine,
9.15 + startPosition = ~ i, endPosition = 0};
9.16 + in PolyML.raiseWithLocation (exn, location) handle e => e end;
9.17 +
9.18 +fun get_exn_serial exn =
9.19 + (case Option.map #startPosition (PolyML.exceptionLocation exn) of
9.20 + NONE => NONE
9.21 + | SOME i => if i >= 0 then NONE else SOME (~ i));
9.22 +
9.23 use "ML-Systems/polyml_common.ML";
9.24 use "ML-Systems/multithreading_polyml.ML";
9.25 use "ML-Systems/unsynchronized.ML";
10.1 --- a/src/Pure/ML-Systems/smlnj.ML Wed Aug 17 14:32:48 2011 -0700
10.2 +++ b/src/Pure/ML-Systems/smlnj.ML Wed Aug 17 23:41:47 2011 +0200
10.3 @@ -3,10 +3,13 @@
10.4 Compatibility file for Standard ML of New Jersey 110 or later.
10.5 *)
10.6
10.7 +use "ML-Systems/proper_int.ML";
10.8 +
10.9 exception Interrupt;
10.10 fun reraise exn = raise exn;
10.11 +fun set_exn_serial (_: int) (exn: exn) = exn;
10.12 +fun get_exn_serial (exn: exn) : int option = NONE;
10.13
10.14 -use "ML-Systems/proper_int.ML";
10.15 use "ML-Systems/overloading_smlnj.ML";
10.16 use "General/exn.ML";
10.17 use "ML-Systems/single_assignment.ML";
11.1 --- a/src/Pure/PIDE/document.ML Wed Aug 17 14:32:48 2011 -0700
11.2 +++ b/src/Pure/PIDE/document.ML Wed Aug 17 23:41:47 2011 +0200
11.3 @@ -372,7 +372,7 @@
11.4 |> set_result result;
11.5 in ((assigns, execs, [(name, node')]), node') end)
11.6 end))
11.7 - |> Future.join_results |> Exn.release_all |> map #1;
11.8 + |> Future.join_results |> Par_Exn.release_all |> map #1;
11.9
11.10 val state' = state
11.11 |> fold (fold define_exec o #2) updates
12.1 --- a/src/Pure/ROOT.ML Wed Aug 17 14:32:48 2011 -0700
12.2 +++ b/src/Pure/ROOT.ML Wed Aug 17 23:41:47 2011 +0200
12.3 @@ -77,7 +77,7 @@
12.4 then use "Concurrent/bash.ML"
12.5 else use "Concurrent/bash_sequential.ML";
12.6
12.7 -use "Concurrent/mailbox.ML";
12.8 +use "Concurrent/par_exn.ML";
12.9 use "Concurrent/task_queue.ML";
12.10 use "Concurrent/future.ML";
12.11
12.12 @@ -89,6 +89,7 @@
12.13 if Multithreading.available then ()
12.14 else use "Concurrent/par_list_sequential.ML";
12.15
12.16 +use "Concurrent/mailbox.ML";
12.17 use "Concurrent/cache.ML";
12.18
12.19
13.1 --- a/src/Pure/Thy/thy_info.ML Wed Aug 17 14:32:48 2011 -0700
13.2 +++ b/src/Pure/Thy/thy_info.ML Wed Aug 17 23:41:47 2011 +0200
13.3 @@ -207,7 +207,7 @@
13.4 " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
13.5 | Finished thy => Future.value (thy, Future.value (), I)))
13.6 #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn])
13.7 - #> rev #> Exn.release_all) #> ignore;
13.8 + #> rev #> Par_Exn.release_all) #> ignore;
13.9
13.10 in
13.11
14.1 --- a/src/Pure/thm.ML Wed Aug 17 14:32:48 2011 -0700
14.2 +++ b/src/Pure/thm.ML Wed Aug 17 23:41:47 2011 +0200
14.3 @@ -515,7 +515,7 @@
14.4 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
14.5 Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
14.6 (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
14.7 -and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
14.8 +and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
14.9
14.10 val join_proofs = Proofterm.join_bodies o map fulfill_body;
14.11