# HG changeset patch
# User wenzelm
# Date 1519035205 -3600
# Node ID 11b390e971f6bc0e20a7c96d93f1b95896ec61e8
# Parent  67e5deb9e2905c25ed8bae28fabc70a897759739
clarified signature;

diff -r 67e5deb9e290 -r 11b390e971f6 src/Pure/Concurrent/multithreading.ML
--- 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;
 
 
diff -r 67e5deb9e290 -r 11b390e971f6 src/Pure/Concurrent/par_list.ML
--- 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;
diff -r 67e5deb9e290 -r 11b390e971f6 src/Pure/PIDE/execution.ML
--- 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));