author | wenzelm |
Mon, 16 Nov 2020 23:49:20 +0100 | |
changeset 72628 | 5e616a454b23 |
parent 72620 | 429afd0d1a79 |
child 72637 | fd68c9c1b90b |
permissions | -rw-r--r-- |
65477 | 1 |
/* Title: Pure/ML/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, |
|
71594 | 16 |
sessions_structure: Sessions.Structure, |
71598 | 17 |
store: Sessions.Store, |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
18 |
logic: String = "", |
71639
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
19 |
raw_ml_system: Boolean = false, |
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
20 |
use_prelude: List[String] = Nil, |
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
21 |
eval_main: String = "", |
62544 | 22 |
args: List[String] = Nil, |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62548
diff
changeset
|
23 |
modes: List[String] = Nil, |
62573 | 24 |
cwd: JFile = null, |
62610
4c89504c76fb
more uniform signature for various process invocations;
wenzelm
parents:
62606
diff
changeset
|
25 |
env: Map[String, String] = Isabelle_System.settings(), |
62557 | 26 |
redirect: Boolean = false, |
62603 | 27 |
cleanup: () => Unit = () => (), |
71598 | 28 |
session_base: Option[Sessions.Base] = None): Bash.Process = |
62544 | 29 |
{ |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
30 |
val logic_name = Isabelle_System.default_logic(logic) |
68209 | 31 |
|
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
32 |
val heaps: List[String] = |
62643 | 33 |
if (raw_ml_system) Nil |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
34 |
else { |
72571 | 35 |
sessions_structure.selection(logic_name). |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
69831
diff
changeset
|
36 |
build_requirements(List(logic_name)). |
71598 | 37 |
map(a => File.platform_path(store.the_heap(a))) |
62544 | 38 |
} |
39 |
||
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
40 |
val eval_init = |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
41 |
if (heaps.isEmpty) { |
62544 | 42 |
List( |
62912 | 43 |
""" |
44 |
fun chapter (_: string) = (); |
|
45 |
fun section (_: string) = (); |
|
46 |
fun subsection (_: string) = (); |
|
47 |
fun subsubsection (_: string) = (); |
|
48 |
fun paragraph (_: string) = (); |
|
49 |
fun subparagraph (_: string) = (); |
|
50 |
val ML_file = PolyML.use; |
|
51 |
""", |
|
62544 | 52 |
if (Platform.is_windows) |
53 |
"fun exit 0 = OS.Process.exit OS.Process.success" + |
|
54 |
" | exit 1 = OS.Process.exit OS.Process.failure" + |
|
55 |
" | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" |
|
62560 | 56 |
else |
57 |
"fun exit rc = Posix.Process.exit (Word8.fromInt rc)", |
|
62629
1815513a57f1
clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents:
62614
diff
changeset
|
58 |
"PolyML.Compiler.prompt1 := \"Poly/ML> \"", |
1815513a57f1
clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents:
62614
diff
changeset
|
59 |
"PolyML.Compiler.prompt2 := \"Poly/ML# \"") |
62544 | 60 |
} |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
61 |
else |
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
62 |
List( |
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
63 |
"(PolyML.SaveState.loadHierarchy " + |
66782 | 64 |
ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
65 |
"; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + |
66782 | 66 |
ML_Syntax.print_string_bytes(": " + logic_name + "\n") + |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
67 |
"); OS.Process.exit OS.Process.failure)") |
62544 | 68 |
|
69 |
val eval_modes = |
|
70 |
if (modes.isEmpty) Nil |
|
66782 | 71 |
else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes)) |
62544 | 72 |
|
73 |
// options |
|
74 |
val isabelle_process_options = Isabelle_System.tmp_file("options") |
|
71114 | 75 |
Isabelle_System.chmod("600", File.path(isabelle_process_options)) |
62544 | 76 |
File.write(isabelle_process_options, YXML.string_of_body(options.encode)) |
62573 | 77 |
val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
78 |
val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") |
62544 | 79 |
|
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65420
diff
changeset
|
80 |
// session base |
72615
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
81 |
val init_session = Isabelle_System.tmp_file("init_session", ext = "ML") |
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
82 |
val init_session_name = init_session.getAbsolutePath |
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
83 |
Isabelle_System.chmod("600", File.path(init_session)) |
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
84 |
File.write(init_session, |
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65420
diff
changeset
|
85 |
session_base match { |
72615
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
86 |
case None => "" |
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65420
diff
changeset
|
87 |
case Some(base) => |
72620 | 88 |
def print_symbols: List[(String, Int)] => String = |
89 |
ML_Syntax.print_list( |
|
90 |
ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_int)) |
|
72617 | 91 |
def print_table: List[(String, String)] => String = |
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65420
diff
changeset
|
92 |
ML_Syntax.print_list( |
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65420
diff
changeset
|
93 |
ML_Syntax.print_pair( |
72617 | 94 |
ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes)) |
72614 | 95 |
def print_list: List[String] => String = |
96 |
ML_Syntax.print_list(ML_Syntax.print_string_bytes) |
|
97 |
def print_sessions: List[(String, Position.T)] => String = |
|
67493
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
98 |
ML_Syntax.print_list( |
72614 | 99 |
ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties)) |
100 |
def print_bibtex_entries: List[(String, List[String])] => String = |
|
72613
d01ea9e3bd2d
clarified bibtex_entries: refer to overall session structure;
wenzelm
parents:
72571
diff
changeset
|
101 |
ML_Syntax.print_list( |
d01ea9e3bd2d
clarified bibtex_entries: refer to overall session structure;
wenzelm
parents:
72571
diff
changeset
|
102 |
ML_Syntax.print_pair(ML_Syntax.print_string_bytes, |
72614 | 103 |
ML_Syntax.print_list(ML_Syntax.print_string_bytes))) |
67493
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
104 |
|
72615
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
105 |
"Resources.init_session" + |
72620 | 106 |
"{html_symbols = " + print_symbols(Symbol.codes) + |
107 |
", session_positions = " + print_sessions(sessions_structure.session_positions) + |
|
71594 | 108 |
", session_directories = " + print_table(sessions_structure.dest_session_directories) + |
72616 | 109 |
", session_chapters = " + print_table(sessions_structure.session_chapters) + |
72613
d01ea9e3bd2d
clarified bibtex_entries: refer to overall session structure;
wenzelm
parents:
72571
diff
changeset
|
110 |
", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) + |
67520 | 111 |
", docs = " + print_list(base.doc_names) + |
67219 | 112 |
", global_theories = " + print_table(base.global_theories.toList) + |
72615
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
113 |
", loaded_theories = " + print_list(base.loaded_theories.keys) + "}" |
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
114 |
}) |
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65420
diff
changeset
|
115 |
|
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65420
diff
changeset
|
116 |
// process |
62544 | 117 |
val eval_process = |
71639
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
118 |
proper_string(eval_main).getOrElse( |
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
119 |
if (heaps.isEmpty) { |
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
120 |
"PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")) |
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
121 |
} |
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
122 |
else "Isabelle_Process.init ()") |
62544 | 123 |
|
62601
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
124 |
// ISABELLE_TMP |
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
125 |
val isabelle_tmp = Isabelle_System.tmp_dir("process") |
72119
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72118
diff
changeset
|
126 |
val env_tmp = |
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72118
diff
changeset
|
127 |
Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp), |
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72118
diff
changeset
|
128 |
"POLYSTATSDIR" -> isabelle_tmp.getAbsolutePath) |
62601
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
129 |
|
71881 | 130 |
val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(",")) |
131 |
||
64274 | 132 |
val ml_runtime_options = |
133 |
{ |
|
134 |
val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) |
|
69702 | 135 |
val ml_options1 = |
136 |
if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options |
|
137 |
else ml_options ::: List("--gcthreads", options.int("threads").toString) |
|
138 |
val ml_options2 = |
|
139 |
if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1 |
|
140 |
else ml_options1 ::: List("--codepage", "utf8") |
|
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
71881
diff
changeset
|
141 |
ml_options2 ::: List("--exportstats") |
64274 | 142 |
} |
143 |
||
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
|
144 |
// 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
|
145 |
val bash_args = |
64274 | 146 |
ml_runtime_options ::: |
72615
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
147 |
(eval_init ::: eval_modes ::: eval_options).flatMap(List("--eval", _)) ::: |
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
148 |
List("--use", init_session_name, |
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
149 |
"--eval", "OS.FileSys.remove " + ML_Syntax.print_string_bytes(init_session_name)) ::: |
71639
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
150 |
use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args |
62546 | 151 |
|
63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
62912
diff
changeset
|
152 |
Bash.process( |
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
62912
diff
changeset
|
153 |
"exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + |
64304 | 154 |
Bash.strings(bash_args), |
62614 | 155 |
cwd = cwd, |
71881 | 156 |
env = env ++ env_options ++ env_tmp ++ env_functions, |
62614 | 157 |
redirect = redirect, |
62602 | 158 |
cleanup = () => |
159 |
{ |
|
160 |
isabelle_process_options.delete |
|
72615
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
161 |
init_session.delete |
62602 | 162 |
Isabelle_System.rm_tree(isabelle_tmp) |
62603 | 163 |
cleanup() |
62602 | 164 |
}) |
62544 | 165 |
} |
62586 | 166 |
|
167 |
||
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
168 |
/* Isabelle tool wrapper */ |
62586 | 169 |
|
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
170 |
val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args => |
62586 | 171 |
{ |
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
172 |
var dirs: List[Path] = Nil |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
173 |
var eval_args: List[String] = Nil |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
174 |
var logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
175 |
var modes: List[String] = Nil |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
176 |
var options = Options.init() |
62586 | 177 |
|
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
178 |
val getopts = Getopts(""" |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
179 |
Usage: isabelle process [OPTIONS] |
62586 | 180 |
|
181 |
Options are: |
|
62677 | 182 |
-T THEORY load theory |
62639 | 183 |
-d DIR include session directory |
62586 | 184 |
-e ML_EXPR evaluate ML expression on startup |
185 |
-f ML_FILE evaluate ML file on startup |
|
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
186 |
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
62586 | 187 |
-m MODE add print mode for output |
188 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
189 |
||
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
190 |
Run the raw Isabelle ML process in batch mode. |
62586 | 191 |
""", |
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
192 |
"T:" -> (arg => |
66782 | 193 |
eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))), |
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
194 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
195 |
"e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
196 |
"f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
197 |
"l:" -> (arg => logic = arg), |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
198 |
"m:" -> (arg => modes = arg :: modes), |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
199 |
"o:" -> (arg => options = options + arg)) |
62586 | 200 |
|
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
201 |
val more_args = getopts(args) |
71383 | 202 |
if (args.isEmpty || more_args.nonEmpty) getopts.usage() |
62586 | 203 |
|
72628
5e616a454b23
clarified Resources.init_session for low-level "isabelle process";
wenzelm
parents:
72620
diff
changeset
|
204 |
val base_info = Sessions.base_info(options, logic, dirs = dirs).check |
71598 | 205 |
val store = Sessions.store(options) |
72557 | 206 |
val result = |
72628
5e616a454b23
clarified Resources.init_session for low-level "isabelle process";
wenzelm
parents:
72620
diff
changeset
|
207 |
ML_Process(options, base_info.sessions_structure, store, logic = logic, args = eval_args, |
5e616a454b23
clarified Resources.init_session for low-level "isabelle process";
wenzelm
parents:
72620
diff
changeset
|
208 |
modes = modes, session_base = Some(base_info.base)) |
72557 | 209 |
.result( |
210 |
progress_stdout = Output.writeln(_, stdout = true), |
|
211 |
progress_stderr = Output.writeln(_)) |
|
212 |
||
213 |
sys.exit(result.rc) |
|
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
214 |
}) |
62544 | 215 |
} |