# HG changeset patch
# User wenzelm
# Date 1598284684 -7200
# Node ID edaed30360cca0d6fe23211d90fef1edffb37cf3
# Parent  8dc2e4d9deaa7990befe9a2c1f183ed934e93994
more flexible default for max_threads;

diff -r 8dc2e4d9deaa -r edaed30360cc src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Mon Aug 24 17:19:41 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Mon Aug 24 17:58:04 2020 +0200
@@ -975,7 +975,7 @@
    is partly due to the JVM and partly due to the ML "bash" function. *)
 val fudge_ms = 250
 
-fun uncached_solve_any_problem overlord deadline max_threads max_solutions problems =
+fun uncached_solve_any_problem overlord deadline max_threads0 max_solutions problems =
   let
     val j = find_index (curry (op =) True o #formula) problems
     val indexed_problems = if j >= 0 then
@@ -987,6 +987,11 @@
                              (0 upto length problems - 1)
     val reindex = fst o nth indexed_problems
 
+    val max_threads =
+      if max_threads0 = 0
+      then Options.default_int \<^system_option>\<open>kodkod_max_threads\<close>
+      else max_threads0
+
     val external_process =
       not (Options.default_bool \<^system_option>\<open>kodkod_scala\<close>) orelse overlord
     val timeout0 = Time.toMilliseconds (deadline - Time.now ())
diff -r 8dc2e4d9deaa -r edaed30360cc src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Mon Aug 24 17:19:41 2020 +0200
+++ b/src/HOL/Tools/etc/options	Mon Aug 24 17:58:04 2020 +0200
@@ -40,3 +40,6 @@
 
 public option kodkod_scala : bool = false
   -- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)"
+
+public option kodkod_max_threads : int = 0
+  -- "default max_threads for Nitpick/Kodkod (0: maximum of Java/Scala platform)"