author | wenzelm |
Mon, 07 Mar 2016 18:31:40 +0100 | |
changeset 62546 | 973b12bccbc5 |
parent 62545 | 8ebffdaf2ce2 |
child 62547 | b33dea503665 |
permissions | -rw-r--r-- |
62544 | 1 |
/* Title: Pure/System/ml_process.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
The underlying ML process. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object ML_Process |
|
11 |
{ |
|
12 |
def apply(options: Options, |
|
13 |
heap: String = "", |
|
14 |
args: List[String] = Nil, |
|
15 |
process_socket: String = "", |
|
16 |
secure: Boolean = false, |
|
17 |
modes: List[String] = Nil): Bash.Process = |
|
18 |
{ |
|
19 |
val load_heaps = |
|
20 |
{ |
|
21 |
if (heap == "RAW_ML_SYSTEM") Nil |
|
22 |
else if (heap.iterator.contains('/')) { |
|
23 |
val heap_path = Path.explode(heap) |
|
24 |
if (!heap_path.is_file) error("Bad heap file: " + heap_path) |
|
25 |
List(heap_path) |
|
26 |
} |
|
27 |
else { |
|
28 |
val dirs = Isabelle_System.find_logics_dirs() |
|
29 |
val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap |
|
30 |
dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match { |
|
31 |
case Some(heap_path) => List(heap_path) |
|
32 |
case None => |
|
33 |
error("Unknown logic " + quote(heap) + " -- no heap file found in:\n" + |
|
34 |
cat_lines(dirs.map(dir => " " + dir.implode))) |
|
35 |
} |
|
36 |
} |
|
37 |
} |
|
38 |
||
39 |
val eval_heaps = |
|
40 |
load_heaps.map(load_heap => |
|
41 |
"PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) + |
|
42 |
" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + |
|
43 |
ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") + |
|
44 |
"); OS.Process.exit OS.Process.failure)") |
|
45 |
||
46 |
val eval_exit = |
|
47 |
if (load_heaps.isEmpty) { |
|
48 |
List( |
|
49 |
if (Platform.is_windows) |
|
50 |
"fun exit 0 = OS.Process.exit OS.Process.success" + |
|
51 |
" | exit 1 = OS.Process.exit OS.Process.failure" + |
|
52 |
" | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" |
|
53 |
else |
|
54 |
"fun exit rc = Posix.Process.exit (Word8.fromInt rc)" |
|
55 |
) |
|
56 |
} |
|
57 |
else Nil |
|
58 |
||
59 |
val eval_secure = if (secure) List("Secure.set_secure ()") else Nil |
|
60 |
||
61 |
val eval_modes = |
|
62 |
if (modes.isEmpty) Nil |
|
63 |
else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes)) |
|
64 |
||
65 |
||
66 |
// options |
|
67 |
val isabelle_process_options = Isabelle_System.tmp_file("options") |
|
68 |
File.write(isabelle_process_options, YXML.string_of_body(options.encode)) |
|
62545
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62544
diff
changeset
|
69 |
val env = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) |
62544 | 70 |
val eval_options = List("Options.load_default ()") |
71 |
||
72 |
val eval_process = |
|
73 |
if (process_socket == "") Nil |
|
74 |
else List("Isabelle_Process.init " + ML_Syntax.print_string_raw(process_socket)) |
|
75 |
||
62545
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62544
diff
changeset
|
76 |
// bash |
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62544
diff
changeset
|
77 |
val bash_args = |
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62544
diff
changeset
|
78 |
Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: |
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62544
diff
changeset
|
79 |
(eval_heaps ::: eval_exit ::: eval_secure ::: eval_modes ::: eval_options ::: eval_process). |
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62544
diff
changeset
|
80 |
map(eval => List("--eval", eval)).flatten ::: args |
62546 | 81 |
|
82 |
Bash.process(env = env, script = |
|
62544 | 83 |
""" |
84 |
[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle |
|
85 |
||
86 |
export ISABELLE_PID="$$" |
|
87 |
export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID" |
|
88 |
mkdir -p "$ISABELLE_TMP" |
|
89 |
chmod $(umask -S) "$ISABELLE_TMP" |
|
90 |
||
91 |
librarypath "$ML_HOME" |
|
62545
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62544
diff
changeset
|
92 |
"$ML_HOME/poly" -q -i """ + File.bash_escape(bash_args) + """ |
62544 | 93 |
RC="$?" |
94 |
||
95 |
rm -f "$ISABELLE_PROCESS_OPTIONS" |
|
96 |
rmdir "$ISABELLE_TMP" |
|
97 |
||
98 |
exit "$RC" |
|
62546 | 99 |
""") |
62544 | 100 |
} |
101 |
} |