author | wenzelm |
Tue, 23 Apr 2024 15:57:03 +0200 | |
changeset 80145 | 0eff7d113549 |
parent 78178 | a177f71dc79f |
permissions | -rw-r--r-- |
65477 | 1 |
/* Title: Pure/ML/ml_console.scala |
62559 | 2 |
Author: Makarius |
3 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
4 |
The raw ML process in interactive mode. |
62559 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
75393 | 10 |
object ML_Console { |
62559 | 11 |
/* command line entry point */ |
12 |
||
75393 | 13 |
def main(args: Array[String]): Unit = { |
62559 | 14 |
Command_Line.tool { |
15 |
var dirs: List[Path] = Nil |
|
68541 | 16 |
var include_sessions: List[String] = Nil |
62559 | 17 |
var logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
18 |
var modes: List[String] = Nil |
|
19 |
var no_build = false |
|
20 |
var options = Options.init() |
|
62643 | 21 |
var raw_ml_system = false |
62559 | 22 |
|
23 |
val getopts = Getopts(""" |
|
24 |
Usage: isabelle console [OPTIONS] |
|
25 |
||
26 |
Options are: |
|
27 |
-d DIR include session directory |
|
68541 | 28 |
-i NAME include session in name-space of theories |
62559 | 29 |
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
30 |
-m MODE add print mode for output |
|
31 |
-n no build of session image on startup |
|
32 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
62643 | 33 |
-r bootstrap from raw Poly/ML |
62559 | 34 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
35 |
Build a logic session image and run the raw Isabelle ML process |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
36 |
in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" + |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
37 |
quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """. |
62559 | 38 |
""", |
39 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
|
68541 | 40 |
"i:" -> (arg => include_sessions = include_sessions ::: List(arg)), |
62559 | 41 |
"l:" -> (arg => logic = arg), |
42 |
"m:" -> (arg => modes = arg :: modes), |
|
72570 | 43 |
"n" -> (_ => no_build = true), |
62559 | 44 |
"o:" -> (arg => options = options + arg), |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
68541
diff
changeset
|
45 |
"r" -> (_ => raw_ml_system = true)) |
62559 | 46 |
|
47 |
val more_args = getopts(args) |
|
71383 | 48 |
if (more_args.nonEmpty) getopts.usage() |
62559 | 49 |
|
50 |
||
78178 | 51 |
val store = Store(options) |
71594 | 52 |
|
68305 | 53 |
// build logic |
54 |
if (!no_build && !raw_ml_system) { |
|
64115 | 55 |
val progress = new Console_Progress() |
68305 | 56 |
val rc = |
68331 | 57 |
progress.interrupt_handler { |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
68541
diff
changeset
|
58 |
Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs) |
68331 | 59 |
} |
74306 | 60 |
if (rc != Process_Result.RC.ok) sys.exit(rc) |
62559 | 61 |
} |
62 |
||
76729 | 63 |
val session_background = |
76655 | 64 |
if (raw_ml_system) { |
76656 | 65 |
Sessions.Background( |
76655 | 66 |
base = Sessions.Base.bootstrap, |
67 |
sessions_structure = Sessions.load_structure(options, dirs = dirs)) |
|
68 |
} |
|
69 |
else { |
|
76656 | 70 |
Sessions.background( |
76655 | 71 |
options, logic, dirs = dirs, include_sessions = include_sessions).check_errors |
72 |
} |
|
73 |
||
77414
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
76729
diff
changeset
|
74 |
val session_heaps = |
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
76729
diff
changeset
|
75 |
if (raw_ml_system) Nil |
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
76729
diff
changeset
|
76 |
else ML_Process.session_heaps(store, session_background, logic = logic) |
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
76729
diff
changeset
|
77 |
|
62559 | 78 |
// process loop |
79 |
val process = |
|
77414
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
76729
diff
changeset
|
80 |
ML_Process(options, session_background, session_heaps, args = List("-i"), redirect = true, |
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
76729
diff
changeset
|
81 |
modes = if (raw_ml_system) Nil else modes ::: List("ASCII")) |
67802 | 82 |
|
73367 | 83 |
POSIX_Interrupt.handler { process.interrupt() } { |
74141 | 84 |
new TTY_Loop(process.stdin, process.stdout).join() |
85 |
val rc = process.join() |
|
74306 | 86 |
if (rc != Process_Result.RC.ok) sys.exit(rc) |
62559 | 87 |
} |
88 |
} |
|
89 |
} |
|
90 |
} |