# HG changeset patch
# User wenzelm
# Date 1460204270 -7200
# Node ID f1bdf10f95d805b57a7413d72e8355becf2b3ff5
# Parent  ce47945ce4fb104109a748f3634a4ee7e8e8d7e7
tuned signature;

diff -r ce47945ce4fb -r f1bdf10f95d8 src/HOL/TPTP/MaSh_Eval.thy
--- a/src/HOL/TPTP/MaSh_Eval.thy	Sat Apr 09 14:11:31 2016 +0200
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Sat Apr 09 14:17:50 2016 +0200
@@ -15,7 +15,7 @@
    lam_trans = combs, timeout = 30, dont_preplay, minimize]
 
 ML {*
-Multithreading.max_threads_value ()
+Multithreading.max_threads ()
 *}
 
 ML {*
diff -r ce47945ce4fb -r f1bdf10f95d8 src/HOL/TPTP/MaSh_Export_Base.thy
--- a/src/HOL/TPTP/MaSh_Export_Base.thy	Sat Apr 09 14:11:31 2016 +0200
+++ b/src/HOL/TPTP/MaSh_Export_Base.thy	Sat Apr 09 14:17:50 2016 +0200
@@ -20,7 +20,7 @@
 hide_fact (open) HOL.ext
 
 ML {*
-Multithreading.max_threads_value ()
+Multithreading.max_threads ()
 *}
 
 ML {*
diff -r ce47945ce4fb -r f1bdf10f95d8 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Apr 09 14:11:31 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Apr 09 14:17:50 2016 +0200
@@ -178,7 +178,7 @@
   [cvc4N, z3N, spassN, eN, vampireN, veritN, e_sineN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
-  |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))
+  |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))
   |> implode_param
 
 fun set_default_raw_param param thy =
diff -r ce47945ce4fb -r f1bdf10f95d8 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat Apr 09 14:11:31 2016 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Apr 09 14:17:50 2016 +0200
@@ -311,7 +311,7 @@
 
     val m =
       if ! do_shutdown andalso Task_Queue.all_passive (! queue) then 0
-      else Multithreading.max_threads_value ();
+      else Multithreading.max_threads ();
     val _ = max_active := m;
     val _ = max_workers := 2 * m;
 
diff -r ce47945ce4fb -r f1bdf10f95d8 src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Sat Apr 09 14:11:31 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Sat Apr 09 14:17:50 2016 +0200
@@ -6,7 +6,7 @@
 
 signature MULTITHREADING =
 sig
-  val max_threads_value: unit -> int
+  val max_threads: unit -> int
   val max_threads_update: int -> unit
   val enabled: unit -> bool
   val sync_wait: Thread.threadAttribute list option -> Time.time option ->
@@ -21,7 +21,9 @@
 structure Multithreading: MULTITHREADING =
 struct
 
-(* options *)
+(* max_threads *)
+
+local
 
 fun num_processors () =
   (case Thread.numPhysicalProcessors () of
@@ -31,11 +33,15 @@
 fun max_threads_result m =
   if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8);
 
-val max_threads = ref 1;
-fun max_threads_value () = ! max_threads;
-fun max_threads_update m = max_threads := max_threads_result m;
+val max_threads_state = ref 1;
+
+in
 
-fun enabled () = max_threads_value () > 1;
+fun max_threads () = ! max_threads_state;
+fun max_threads_update m = max_threads_state := max_threads_result m;
+fun enabled () = max_threads () > 1;
+
+end;
 
 
 (* synchronous wait *)
diff -r ce47945ce4fb -r f1bdf10f95d8 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Apr 09 14:11:31 2016 +0200
+++ b/src/Pure/Tools/build.ML	Sat Apr 09 14:17:50 2016 +0200
@@ -51,7 +51,7 @@
     val y = f x;
     val timing = Timing.result start;
 
-    val threads = string_of_int (Multithreading.max_threads_value ());
+    val threads = string_of_int (Multithreading.max_threads ());
     val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
       |> Real.fmt (StringCvt.FIX (SOME 2));