author | wenzelm |
Sat, 12 Mar 2016 21:23:58 +0100 | |
changeset 62601 | a937889f0086 |
parent 62600 | 614aefb0e6cc |
child 62602 | 96e679f042ec |
permissions | -rw-r--r-- |
62586 | 1 |
/* Title: Pure/Tools/ml_process.scala |
62544 | 2 |
Author: Makarius |
3 |
||
62586 | 4 |
The raw ML process. |
62544 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
62573 | 10 |
import java.io.{File => JFile} |
11 |
||
12 |
||
62544 | 13 |
object ML_Process |
14 |
{ |
|
15 |
def apply(options: Options, |
|
16 |
heap: String = "", |
|
17 |
args: List[String] = Nil, |
|
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62548
diff
changeset
|
18 |
modes: List[String] = Nil, |
62544 | 19 |
secure: Boolean = false, |
62573 | 20 |
cwd: JFile = null, |
21 |
env: Map[String, String] = Map.empty, |
|
62557 | 22 |
redirect: Boolean = false, |
62564 | 23 |
channel: Option[System_Channel] = None): Bash.Process = |
62544 | 24 |
{ |
25 |
val load_heaps = |
|
26 |
{ |
|
27 |
if (heap == "RAW_ML_SYSTEM") Nil |
|
28 |
else if (heap.iterator.contains('/')) { |
|
29 |
val heap_path = Path.explode(heap) |
|
30 |
if (!heap_path.is_file) error("Bad heap file: " + heap_path) |
|
31 |
List(heap_path) |
|
32 |
} |
|
33 |
else { |
|
34 |
val dirs = Isabelle_System.find_logics_dirs() |
|
35 |
val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap |
|
36 |
dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match { |
|
37 |
case Some(heap_path) => List(heap_path) |
|
38 |
case None => |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
39 |
error("Unknown logic " + quote(heap_name) + " -- no heap file found in:\n" + |
62544 | 40 |
cat_lines(dirs.map(dir => " " + dir.implode))) |
41 |
} |
|
42 |
} |
|
43 |
} |
|
44 |
||
45 |
val eval_heaps = |
|
46 |
load_heaps.map(load_heap => |
|
62576 | 47 |
"(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) + |
48 |
"; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + |
|
62544 | 49 |
ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") + |
50 |
"); OS.Process.exit OS.Process.failure)") |
|
51 |
||
62560 | 52 |
val eval_initial = |
62544 | 53 |
if (load_heaps.isEmpty) { |
54 |
List( |
|
55 |
if (Platform.is_windows) |
|
56 |
"fun exit 0 = OS.Process.exit OS.Process.success" + |
|
57 |
" | exit 1 = OS.Process.exit OS.Process.failure" + |
|
58 |
" | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" |
|
62560 | 59 |
else |
60 |
"fun exit rc = Posix.Process.exit (Word8.fromInt rc)", |
|
61 |
"PolyML.Compiler.prompt1 := \"ML> \"", |
|
62576 | 62 |
"PolyML.Compiler.prompt2 := \"ML# \"") |
62544 | 63 |
} |
64 |
else Nil |
|
65 |
||
66 |
val eval_modes = |
|
67 |
if (modes.isEmpty) Nil |
|
68 |
else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes)) |
|
69 |
||
70 |
// options |
|
71 |
val isabelle_process_options = Isabelle_System.tmp_file("options") |
|
72 |
File.write(isabelle_process_options, YXML.string_of_body(options.encode)) |
|
62573 | 73 |
val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) |
62547 | 74 |
val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()") |
62544 | 75 |
|
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62548
diff
changeset
|
76 |
val eval_secure = if (secure) List("Secure.set_secure ()") else Nil |
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62548
diff
changeset
|
77 |
|
62544 | 78 |
val eval_process = |
62576 | 79 |
if (load_heaps.isEmpty) |
80 |
List("PolyML.print_depth 10") |
|
62565 | 81 |
else |
82 |
channel match { |
|
83 |
case None => |
|
62576 | 84 |
List("(default_print_depth 10; Isabelle_Process.init_options ())") |
62565 | 85 |
case Some(ch) => |
62576 | 86 |
List("(default_print_depth 10; Isabelle_Process.init_protocol " + |
87 |
ML_Syntax.print_string_raw(ch.server_name) + ")") |
|
62565 | 88 |
} |
62544 | 89 |
|
62601
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
90 |
// ISABELLE_TMP |
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
91 |
val isabelle_tmp = Isabelle_System.tmp_dir("process") |
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
92 |
val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp)) |
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
93 |
|
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
|
94 |
// 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
|
95 |
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
|
96 |
Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: |
62560 | 97 |
(eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process). |
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
|
98 |
map(eval => List("--eval", eval)).flatten ::: args |
62546 | 99 |
|
62573 | 100 |
Bash.process( |
62544 | 101 |
""" |
102 |
librarypath "$ML_HOME" |
|
62577
7e2aa1d67dd8
clarified interactive mode, which is relevant for ML prompts;
wenzelm
parents:
62576
diff
changeset
|
103 |
"$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """ |
62544 | 104 |
RC="$?" |
105 |
||
62601
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
106 |
[ -e "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS" |
62544 | 107 |
rmdir "$ISABELLE_TMP" |
108 |
||
109 |
exit "$RC" |
|
62601
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
110 |
""", cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect) |
62544 | 111 |
} |
62586 | 112 |
|
113 |
||
114 |
/* command line entry point */ |
|
115 |
||
116 |
def main(args: Array[String]) |
|
117 |
{ |
|
118 |
Command_Line.tool { |
|
119 |
var eval_args: List[String] = Nil |
|
120 |
var modes: List[String] = Nil |
|
121 |
var options = Options.init() |
|
122 |
||
123 |
val getopts = Getopts(""" |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
124 |
Usage: isabelle process [OPTIONS] [HEAP] |
62586 | 125 |
|
126 |
Options are: |
|
127 |
-e ML_EXPR evaluate ML expression on startup |
|
128 |
-f ML_FILE evaluate ML file on startup |
|
129 |
-m MODE add print mode for output |
|
130 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
131 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
132 |
Run the raw Isabelle ML process in batch mode, using a given heap image. |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
133 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
134 |
If HEAP is a plain name (default ISABELLE_LOGIC=""" + |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
135 |
quote(Isabelle_System.getenv("ISABELLE_LOGIC")) + """), it is searched in |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
136 |
ISABELLE_PATH; if it contains a slash, it is taken as literal file; |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
137 |
if it is "RAW_ML_SYSTEM", the initial ML heap is used. |
62586 | 138 |
""", |
139 |
"e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), |
|
140 |
"f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), |
|
141 |
"m:" -> (arg => modes = arg :: modes), |
|
142 |
"o:" -> (arg => options = options + arg)) |
|
143 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
144 |
if (args.isEmpty) getopts.usage() |
62586 | 145 |
val heap = |
146 |
getopts(args) match { |
|
147 |
case Nil => "" |
|
148 |
case List(heap) => heap |
|
149 |
case _ => getopts.usage() |
|
150 |
} |
|
151 |
||
152 |
ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes). |
|
153 |
result().print_stdout.rc |
|
154 |
} |
|
155 |
} |
|
62544 | 156 |
} |