# HG changeset patch
# User wenzelm
# Date 1415812718 -3600
# Node ID 302104d8366b72e680aa8e859b16f9660ff80f06
# Parent  584077922200d7fb04ffe6dee37f99a7f19f4b81
prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;

diff -r 584077922200 -r 302104d8366b src/HOL/Tools/Function/fun_cases.ML
--- a/src/HOL/Tools/Function/fun_cases.ML	Wed Nov 12 11:39:27 2014 +0100
+++ b/src/HOL/Tools/Function/fun_cases.ML	Wed Nov 12 18:18:38 2014 +0100
@@ -45,7 +45,7 @@
   let
     val thmss =
       map snd args
-      |> burrow (grouped 10 Par_List.map (mk_fun_cases lthy o prep_prop lthy));
+      |> burrow (grouped 10 Par_List.map_independent (mk_fun_cases lthy o prep_prop lthy));
     val facts =
       map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])]))
         args thmss;
diff -r 584077922200 -r 302104d8366b src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Nov 12 11:39:27 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Wed Nov 12 18:18:38 2014 +0100
@@ -585,7 +585,7 @@
   let
     val thmss =
       map snd args
-      |> burrow (grouped 10 Par_List.map (mk_cases lthy o prep_prop lthy));
+      |> burrow (grouped 10 Par_List.map_independent (mk_cases lthy o prep_prop lthy));
     val facts =
       map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])]))
         args thmss;
diff -r 584077922200 -r 302104d8366b src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Wed Nov 12 11:39:27 2014 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Wed Nov 12 18:18:38 2014 +0100
@@ -18,6 +18,7 @@
 sig
   val managed_results: string -> ('a -> 'b) -> 'a list -> 'b Exn.result list
   val map_name: string -> ('a -> 'b) -> 'a list -> 'b list
+  val map_independent: ('a -> 'b) -> 'a list -> 'b list
   val map: ('a -> 'b) -> 'a list -> 'b list
   val get_some: ('a -> 'b option) -> 'a list -> 'b option
   val find_some: ('a -> bool) -> 'a list -> 'a option
@@ -51,6 +52,7 @@
 
 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 map_independent f = map (Exn.interruptible_capture f) #> Par_Exn.release_all;
 
 fun get_some f xs =
   let
diff -r 584077922200 -r 302104d8366b src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Nov 12 11:39:27 2014 +0100
+++ b/src/Pure/Isar/specification.ML	Wed Nov 12 18:18:38 2014 +0100
@@ -117,8 +117,7 @@
 
     val Asss =
       (map o map) snd raw_specss
-      |> (burrow o burrow)
-        (grouped 10 (Par_List.map_name "Specification.parse_prop") (parse_prop params_ctxt));
+      |> (burrow o burrow) (grouped 10 Par_List.map_independent (parse_prop params_ctxt));
     val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
       |> fold Name.declare xs;
     val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names);
diff -r 584077922200 -r 302104d8366b src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Nov 12 11:39:27 2014 +0100
+++ b/src/Pure/Syntax/syntax.ML	Wed Nov 12 18:18:38 2014 +0100
@@ -273,13 +273,13 @@
 fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
 
 fun read_typs ctxt =
-  grouped 10 (Par_List.map_name "Syntax.read_typs") (parse_typ ctxt) #> check_typs ctxt;
+  grouped 10 Par_List.map_independent (parse_typ ctxt) #> check_typs ctxt;
 
 fun read_terms ctxt =
-  grouped 10 (Par_List.map_name "Syntax.read_terms") (parse_term ctxt) #> check_terms ctxt;
+  grouped 10 Par_List.map_independent (parse_term ctxt) #> check_terms ctxt;
 
 fun read_props ctxt =
-  grouped 10 (Par_List.map_name "Syntax.read_props") (parse_prop ctxt) #> check_props ctxt;
+  grouped 10 Par_List.map_independent (parse_prop ctxt) #> check_props ctxt;
 
 val read_typ = singleton o read_typs;
 val read_term = singleton o read_terms;