--- a/src/Pure/Concurrent/multithreading.ML Mon Feb 19 10:35:53 2018 +0100
+++ b/src/Pure/Concurrent/multithreading.ML Mon Feb 19 11:13:25 2018 +0100
@@ -9,6 +9,7 @@
val max_threads: unit -> int
val max_threads_update: int -> unit
val enabled: unit -> bool
+ val relevant: 'a list -> bool
val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
val trace: int ref
val tracing: int -> (unit -> string) -> unit
@@ -41,6 +42,8 @@
fun max_threads_update m = max_threads_state := max_threads_result m;
fun enabled () = max_threads () > 1;
+val relevant = (fn [] => false | [_] => false | _ => enabled ());
+
end;
--- a/src/Pure/Concurrent/par_list.ML Mon Feb 19 10:35:53 2018 +0100
+++ b/src/Pure/Concurrent/par_list.ML Mon Feb 19 11:13:25 2018 +0100
@@ -29,9 +29,9 @@
struct
fun forked_results name f xs =
- if null xs orelse null (tl xs) orelse not (Multithreading.enabled ())
- then map (Exn.capture f) xs
- else Future.forked_results {name = name, deps = []} (map (fn x => fn () => f x) xs);
+ if Multithreading.relevant xs
+ then Future.forked_results {name = name, deps = []} (map (fn x => fn () => f x) xs)
+ else map (Exn.capture f) 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;
--- a/src/Pure/PIDE/execution.ML Mon Feb 19 10:35:53 2018 +0100
+++ b/src/Pure/PIDE/execution.ML Mon Feb 19 11:13:25 2018 +0100
@@ -162,13 +162,12 @@
fun fork_prints exec_id =
(case Inttab.lookup (#2 (get_state ())) exec_id of
SOME (_, prints) =>
- if null prints orelse null (tl prints) orelse not (Multithreading.enabled ())
- then List.app (fn {body, ...} => body ()) (rev prints)
- else
+ if Multithreading.relevant prints then
let val pos = Position.thread_data () in
List.app (fn {name, pri, body} =>
ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints)
end
+ else List.app (fn {body, ...} => body ()) (rev prints)
| NONE => raise Fail (unregistered exec_id));