# HG changeset patch
# User wenzelm
# Date 1620824151 -7200
# Node ID b9aae426e51dca7ed3cc119e2ca621fd6d6e39f0
# Parent  c17253cad5c6555c1ca274ba7318e977549f9a81
clarified signature (see Scala version);

diff -r c17253cad5c6 -r b9aae426e51d src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Wed May 12 13:10:13 2021 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Wed May 12 14:55:51 2021 +0200
@@ -16,7 +16,7 @@
 
 signature PAR_LIST =
 sig
-  val map_name: string -> ('a -> 'b) -> 'a list -> 'b list
+  val map': {name: string, sequential: bool} -> ('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
@@ -28,20 +28,22 @@
 structure Par_List: PAR_LIST =
 struct
 
-fun forked_results name f xs =
-  if Future.relevant xs
-  then Future.forked_results {name = name, deps = []} (map (fn x => fn () => f x) xs)
-  else map (Exn.capture f) xs;
+fun managed_results {name, sequential} f xs =
+  if sequential orelse not (Future.relevant xs) then map (Exn.capture f) xs
+  else
+    Future.forked_results
+     {name = if name = "" then "Par_List.map" else name, deps = []}
+     (map (fn x => fn () => f x) xs);
 
-fun map_name name f xs = Par_Exn.release_first (forked_results name f xs);
-fun map f = map_name "Par_List.map" f;
+fun map' params f xs = Par_Exn.release_first (managed_results params f xs);
+fun map f = map' {name = "", sequential = false} f;
 fun map_independent f = map (Exn.interruptible_capture f) #> Par_Exn.release_all;
 
 fun get_some f xs =
   let
     exception FOUND of 'b;
     val results =
-      forked_results "Par_List.get_some"
+      managed_results {name = "Par_List.get_some", sequential = false}
         (fn x => (case f x of NONE => () | SOME y => raise FOUND y)) xs;
   in
     (case get_first (fn Exn.Exn (FOUND res) => SOME res | _ => NONE) results of
diff -r c17253cad5c6 -r b9aae426e51d src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed May 12 13:10:13 2021 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed May 12 14:55:51 2021 +0200
@@ -421,10 +421,9 @@
             (Syntax.check_term (Proof_Context.allow_dummies ctxt) (constrain t); Exn.Res t)
               handle exn as ERROR _ => Exn.Exn exn;
 
+          fun par_map xs = Par_List.map' {name = "Syntax_Phases.parse_term", sequential = false} xs;
           val results' =
-            if parsed_len > 1 then
-              (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_res)
-                check results
+            if parsed_len > 1 then (grouped 10 par_map o apsnd o Exn.maps_res) check results
             else results;
           val reports' = fst (hd results');