equal
deleted
inserted
replaced
96 val bash_args = |
96 val bash_args = |
97 Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: |
97 Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: |
98 (eval_init ::: eval_modes ::: eval_options ::: eval_process). |
98 (eval_init ::: eval_modes ::: eval_options ::: eval_process). |
99 map(eval => List("--eval", eval)).flatten ::: args |
99 map(eval => List("--eval", eval)).flatten ::: args |
100 |
100 |
101 Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args), |
101 Bash.process( |
|
102 "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + |
|
103 File.bash_args(bash_args), |
102 cwd = cwd, |
104 cwd = cwd, |
103 env = |
105 env = |
104 Isabelle_System.library_path(env ++ env_options ++ env_tmp, |
106 Isabelle_System.library_path(env ++ env_options ++ env_tmp, |
105 Isabelle_System.getenv_strict("ML_HOME")), |
107 Isabelle_System.getenv_strict("ML_HOME")), |
106 redirect = redirect, |
108 redirect = redirect, |