# HG changeset patch
# User wenzelm
# Date 1476709246 -7200
# Node ID c8990e5feac9ea91a05bfab981b380504d843344
# Parent  4699d3b3173e74919c70cd686e8a7cd901d56bf8
re-use "threads" for --gcthreads;

diff -r 4699d3b3173e -r c8990e5feac9 NEWS
--- 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.
 
diff -r 4699d3b3173e -r c8990e5feac9 src/Pure/Tools/ml_process.scala
--- 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