|
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)) |
|
69 val bash_env = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) |
|
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 |
|
76 val bash_script = |
|
77 """ |
|
78 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle |
|
79 |
|
80 export ISABELLE_PID="$$" |
|
81 export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID" |
|
82 mkdir -p "$ISABELLE_TMP" |
|
83 chmod $(umask -S) "$ISABELLE_TMP" |
|
84 |
|
85 librarypath "$ML_HOME" |
|
86 "$ML_HOME/poly" -q -i $ML_OPTIONS "$@" |
|
87 RC="$?" |
|
88 |
|
89 rm -f "$ISABELLE_PROCESS_OPTIONS" |
|
90 rmdir "$ISABELLE_TMP" |
|
91 |
|
92 exit "$RC" |
|
93 """ |
|
94 |
|
95 val bash_args = |
|
96 List("-c", bash_script, "ml_process") ::: |
|
97 (eval_heaps ::: eval_exit ::: eval_secure ::: eval_modes ::: eval_options ::: eval_process). |
|
98 map(eval => List("--eval", eval)).flatten ::: args |
|
99 |
|
100 Bash.process(null, bash_env, false, bash_args:_*) |
|
101 } |
|
102 } |