# HG changeset patch
# User blanchet
# Date 1380878908 -7200
# Node ID 903ab115e9fd668a20d6827d8e2fffefe4f18a8f
# Parent  2828f17fa41afd9c8ff6aac38321a8eafbc63ad5
count remote threads as well when balancing CPU usage -- otherwise jEdit users and other users of the "blocking" mode may have to wait for 2 * timeout if they e.g. have 4 cores and 5 provers (the typical situation)

diff -r 2828f17fa41a -r 903ab115e9fd src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 04 18:51:47 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 04 11:28:28 2013 +0200
@@ -194,33 +194,12 @@
   fun merge data : T = AList.merge (op =) (K true) data
 )
 
-fun avoid_too_many_threads _ _ [] = []
-  | avoid_too_many_threads _ (0, 0) _ = []
-  | avoid_too_many_threads ctxt (0, max_remote) provers =
-    provers
-    |> map_filter (remotify_prover_if_supported_and_not_already_remote ctxt)
-    |> take max_remote
-  | avoid_too_many_threads _ (max_local, 0) provers =
-    provers
-    |> filter_out (String.isPrefix remote_prefix)
-    |> take max_local
-  | avoid_too_many_threads ctxt max_local_and_remote (prover :: provers) =
-    let
-      val max_local_and_remote =
-        max_local_and_remote
-        |> (if String.isPrefix remote_prefix prover then apsnd else apfst)
-               (Integer.add ~1)
-    in prover :: avoid_too_many_threads ctxt max_local_and_remote provers end
-
-val max_default_remote_threads = 4
-
 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    timeout, it makes sense to put E first. *)
 fun default_provers_param_value ctxt =
   [eN, spassN, vampireN, z3N, e_sineN, yicesN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
-  |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
-                                  max_default_remote_threads)
+  |> take (Multithreading.max_threads_value ())
   |> implode_param
 
 fun set_default_raw_param param thy =