author | wenzelm |
Tue, 13 Mar 2018 18:28:12 +0100 | |
changeset 67846 | bdf6933f7ac9 |
parent 67808 | 9cb7f5f0bf41 |
child 68209 | aeffd8f1f079 |
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 |
||
10 |
object ML_Console |
|
11 |
{ |
|
12 |
/* command line entry point */ |
|
13 |
||
14 |
def main(args: Array[String]) |
|
15 |
{ |
|
16 |
Command_Line.tool { |
|
17 |
var dirs: List[Path] = Nil |
|
18 |
var logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
|
19 |
var modes: List[String] = Nil |
|
20 |
var no_build = false |
|
21 |
var options = Options.init() |
|
62643 | 22 |
var raw_ml_system = false |
62559 | 23 |
var system_mode = false |
24 |
||
25 |
val getopts = Getopts(""" |
|
26 |
Usage: isabelle console [OPTIONS] |
|
27 |
||
28 |
Options are: |
|
29 |
-d DIR include session directory |
|
30 |
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
|
31 |
-m MODE add print mode for output |
|
32 |
-n no build of session image on startup |
|
33 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
62643 | 34 |
-r bootstrap from raw Poly/ML |
62559 | 35 |
-s system build mode for session image |
36 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
37 |
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
|
38 |
in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" + |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
39 |
quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """. |
62559 | 40 |
""", |
41 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
|
42 |
"l:" -> (arg => logic = arg), |
|
43 |
"m:" -> (arg => modes = arg :: modes), |
|
44 |
"n" -> (arg => no_build = true), |
|
45 |
"o:" -> (arg => options = options + arg), |
|
62643 | 46 |
"r" -> (_ => raw_ml_system = true), |
62559 | 47 |
"s" -> (_ => system_mode = true)) |
48 |
||
49 |
val more_args = getopts(args) |
|
50 |
if (!more_args.isEmpty) getopts.usage() |
|
51 |
||
52 |
||
53 |
// build |
|
62643 | 54 |
if (!no_build && !raw_ml_system && |
67846 | 55 |
!Build.build(options, build_heap = true, no_build = true, |
62641 | 56 |
dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok) |
62559 | 57 |
{ |
64115 | 58 |
val progress = new Console_Progress() |
62559 | 59 |
progress.echo("Build started for Isabelle/" + logic + " ...") |
60 |
progress.interrupt_handler { |
|
62641 | 61 |
val res = |
67846 | 62 |
Build.build(options, progress = progress, build_heap = true, |
62559 | 63 |
dirs = dirs, system_mode = system_mode, sessions = List(logic)) |
62641 | 64 |
if (!res.ok) sys.exit(res.rc) |
62559 | 65 |
} |
66 |
} |
|
67 |
||
68 |
// process loop |
|
69 |
val process = |
|
64598 | 70 |
ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true, |
62643 | 71 |
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"), |
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
64598
diff
changeset
|
72 |
raw_ml_system = raw_ml_system, store = Sessions.store(system_mode), |
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
64598
diff
changeset
|
73 |
session_base = |
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
64598
diff
changeset
|
74 |
if (raw_ml_system) None |
66989 | 75 |
else Some(Sessions.base_info(options, logic, dirs = dirs).check_base)) |
67802 | 76 |
|
67808 | 77 |
val tty_loop = new TTY_Loop(process.stdin, process.stdout, Some(process.interrupt _)) |
62559 | 78 |
val process_result = Future.thread[Int]("process_result") { |
79 |
val rc = process.join |
|
67803 | 80 |
tty_loop.cancel // FIXME does not quite work, cannot interrupt blocking read on System.in |
62559 | 81 |
rc |
82 |
} |
|
67802 | 83 |
tty_loop.join |
62562
905a5db3932d
back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents:
62561
diff
changeset
|
84 |
process_result.join |
62559 | 85 |
} |
86 |
} |
|
87 |
} |