85 case Some(ch) => |
85 case Some(ch) => |
86 List("(default_print_depth 10; Isabelle_Process.init_protocol " + |
86 List("(default_print_depth 10; Isabelle_Process.init_protocol " + |
87 ML_Syntax.print_string_raw(ch.server_name) + ")") |
87 ML_Syntax.print_string_raw(ch.server_name) + ")") |
88 } |
88 } |
89 |
89 |
|
90 // ISABELLE_TMP |
|
91 val isabelle_tmp = Isabelle_System.tmp_dir("process") |
|
92 val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp)) |
|
93 |
90 // bash |
94 // bash |
91 val bash_args = |
95 val bash_args = |
92 Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: |
96 Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: |
93 (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process). |
97 (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process). |
94 map(eval => List("--eval", eval)).flatten ::: args |
98 map(eval => List("--eval", eval)).flatten ::: args |
95 |
99 |
96 Bash.process( |
100 Bash.process( |
97 """ |
101 """ |
98 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle |
|
99 |
|
100 export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$" |
|
101 mkdir -p "$ISABELLE_TMP" |
|
102 chmod $(umask -S) "$ISABELLE_TMP" |
|
103 |
|
104 librarypath "$ML_HOME" |
102 librarypath "$ML_HOME" |
105 "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """ |
103 "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """ |
106 RC="$?" |
104 RC="$?" |
107 |
105 |
108 rm -f "$ISABELLE_PROCESS_OPTIONS" |
106 [ -e "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS" |
109 rmdir "$ISABELLE_TMP" |
107 rmdir "$ISABELLE_TMP" |
110 |
108 |
111 exit "$RC" |
109 exit "$RC" |
112 """, cwd = cwd, env = env ++ env_options, redirect = redirect) |
110 """, cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect) |
113 } |
111 } |
114 |
112 |
115 |
113 |
116 /* command line entry point */ |
114 /* command line entry point */ |
117 |
115 |