equal
deleted
inserted
replaced
90 |
90 |
91 // ISABELLE_TMP |
91 // ISABELLE_TMP |
92 val isabelle_tmp = Isabelle_System.tmp_dir("process") |
92 val isabelle_tmp = Isabelle_System.tmp_dir("process") |
93 val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp)) |
93 val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp)) |
94 |
94 |
|
95 val ml_runtime_options = |
|
96 { |
|
97 val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) |
|
98 if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options |
|
99 else ml_options ::: List("--gcthreads", options.int("threads").toString) |
|
100 } |
|
101 |
95 // bash |
102 // bash |
96 val bash_args = |
103 val bash_args = |
97 Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: |
104 ml_runtime_options ::: |
98 (eval_init ::: eval_modes ::: eval_options ::: eval_process). |
105 (eval_init ::: eval_modes ::: eval_options ::: eval_process). |
99 map(eval => List("--eval", eval)).flatten ::: args |
106 map(eval => List("--eval", eval)).flatten ::: args |
100 |
107 |
101 Bash.process( |
108 Bash.process( |
102 "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + |
109 "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + |