re-use "threads" for --gcthreads;
authorwenzelm
Mon Oct 17 15:00:46 2016 +0200 (2016-10-17)
changeset 64274c8990e5feac9
parent 64266 4699d3b3173e
child 64275 ac2abc987cf9
re-use "threads" for --gcthreads;
NEWS
src/Pure/Tools/ml_process.scala
     1.1 --- a/NEWS	Mon Oct 17 11:07:01 2016 +0200
     1.2 +++ b/NEWS	Mon Oct 17 15:00:46 2016 +0200
     1.3 @@ -992,6 +992,10 @@
     1.4  given heap image. Errors lead to premature exit of the ML process with
     1.5  return code 1.
     1.6  
     1.7 +* The system option "threads" (for the size of the Isabelle/ML thread
     1.8 +farm) is also passed to the underlying ML runtime system as --gcthreads,
     1.9 +unless there is already a default provided via ML_OPTIONS settings.
    1.10 +
    1.11  * Command-line tool "isabelle console" provides option -r to help to
    1.12  bootstrapping Isabelle/Pure interactively.
    1.13  
     2.1 --- a/src/Pure/Tools/ml_process.scala	Mon Oct 17 11:07:01 2016 +0200
     2.2 +++ b/src/Pure/Tools/ml_process.scala	Mon Oct 17 15:00:46 2016 +0200
     2.3 @@ -92,9 +92,16 @@
     2.4      val isabelle_tmp = Isabelle_System.tmp_dir("process")
     2.5      val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
     2.6  
     2.7 +    val ml_runtime_options =
     2.8 +    {
     2.9 +      val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
    2.10 +      if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
    2.11 +      else ml_options ::: List("--gcthreads", options.int("threads").toString)
    2.12 +    }
    2.13 +
    2.14      // bash
    2.15      val bash_args =
    2.16 -      Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
    2.17 +      ml_runtime_options :::
    2.18        (eval_init ::: eval_modes ::: eval_options ::: eval_process).
    2.19          map(eval => List("--eval", eval)).flatten ::: args
    2.20