equal
deleted
inserted
replaced
96 |
96 |
97 // ISABELLE_TMP |
97 // ISABELLE_TMP |
98 val isabelle_tmp = Isabelle_System.tmp_dir("process") |
98 val isabelle_tmp = Isabelle_System.tmp_dir("process") |
99 |
99 |
100 val ml_runtime_options = { |
100 val ml_runtime_options = { |
101 val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) |
101 val ml_options0 = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) |
102 val ml_options1 = |
102 val ml_options1 = |
103 if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options |
103 if (ml_options0.exists(_.containsSlice("gcthreads"))) ml_options0 |
104 else ml_options ::: List("--gcthreads", options.int("threads").toString) |
104 else ml_options0 ::: List("--gcthreads", options.int("threads").toString) |
105 val ml_options2 = |
105 val ml_options2 = |
106 if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1 |
106 if (!Platform.is_windows || ml_options0.exists(_.containsSlice("codepage"))) ml_options1 |
107 else ml_options1 ::: List("--codepage", "utf8") |
107 else ml_options1 ::: List("--codepage", "utf8") |
108 ml_options2 ::: List("--exportstats") |
108 ml_options2 ::: List("--exportstats") |
109 } |
109 } |
110 |
110 |
111 // bash |
111 // bash |