--- a/NEWS Mon Oct 17 11:07:01 2016 +0200
+++ b/NEWS Mon Oct 17 15:00:46 2016 +0200
@@ -992,6 +992,10 @@
given heap image. Errors lead to premature exit of the ML process with
return code 1.
+* The system option "threads" (for the size of the Isabelle/ML thread
+farm) is also passed to the underlying ML runtime system as --gcthreads,
+unless there is already a default provided via ML_OPTIONS settings.
+
* Command-line tool "isabelle console" provides option -r to help to
bootstrapping Isabelle/Pure interactively.
--- a/src/Pure/Tools/ml_process.scala Mon Oct 17 11:07:01 2016 +0200
+++ b/src/Pure/Tools/ml_process.scala Mon Oct 17 15:00:46 2016 +0200
@@ -92,9 +92,16 @@
val isabelle_tmp = Isabelle_System.tmp_dir("process")
val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
+ val ml_runtime_options =
+ {
+ val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
+ if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
+ else ml_options ::: List("--gcthreads", options.int("threads").toString)
+ }
+
// bash
val bash_args =
- Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
+ ml_runtime_options :::
(eval_init ::: eval_modes ::: eval_options ::: eval_process).
map(eval => List("--eval", eval)).flatten ::: args