author | wenzelm |
Wed, 16 Mar 2016 11:45:25 +0100 | |
changeset 62634 | aa3b47b32100 |
parent 62633 | e57416b649d5 |
child 62641 | 0b1b7465f2ef |
permissions | -rw-r--r-- |
62559 | 1 |
/* Title: Pure/Tools/ml_console.scala |
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 |
||
62562
905a5db3932d
back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents:
62561
diff
changeset
|
10 |
import java.io.{IOException, BufferedReader, InputStreamReader} |
62559 | 11 |
|
12 |
||
13 |
object ML_Console |
|
14 |
{ |
|
15 |
/* command line entry point */ |
|
16 |
||
17 |
def main(args: Array[String]) |
|
18 |
{ |
|
19 |
Command_Line.tool { |
|
20 |
var dirs: List[Path] = Nil |
|
21 |
var logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
|
22 |
var modes: List[String] = Nil |
|
23 |
var no_build = false |
|
24 |
var options = Options.init() |
|
25 |
var system_mode = false |
|
26 |
||
27 |
val getopts = Getopts(""" |
|
28 |
Usage: isabelle console [OPTIONS] |
|
29 |
||
30 |
Options are: |
|
31 |
-d DIR include session directory |
|
32 |
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
|
33 |
-m MODE add print mode for output |
|
34 |
-n no build of session image on startup |
|
35 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
36 |
-r logic session is "RAW_ML_SYSTEM" |
62559 | 37 |
-s system build mode for session image |
38 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
39 |
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
|
40 |
in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" + |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
41 |
quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """. |
62559 | 42 |
""", |
43 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
|
44 |
"l:" -> (arg => logic = arg), |
|
45 |
"m:" -> (arg => modes = arg :: modes), |
|
46 |
"n" -> (arg => no_build = true), |
|
47 |
"o:" -> (arg => options = options + arg), |
|
48 |
"r" -> (_ => logic = "RAW_ML_SYSTEM"), |
|
49 |
"s" -> (_ => system_mode = true)) |
|
50 |
||
51 |
val more_args = getopts(args) |
|
52 |
if (!more_args.isEmpty) getopts.usage() |
|
53 |
||
54 |
||
55 |
// build |
|
56 |
if (!no_build && logic != "RAW_ML_SYSTEM" && |
|
57 |
Build.build(options = options, build_heap = true, no_build = true, |
|
58 |
dirs = dirs, system_mode = system_mode, sessions = List(logic)) != 0) |
|
59 |
{ |
|
60 |
val progress = new Console_Progress |
|
61 |
progress.echo("Build started for Isabelle/" + logic + " ...") |
|
62 |
progress.interrupt_handler { |
|
63 |
val rc = |
|
64 |
Build.build(options = options, progress = progress, build_heap = true, |
|
65 |
dirs = dirs, system_mode = system_mode, sessions = List(logic)) |
|
66 |
if (rc != 0) sys.exit(rc) |
|
67 |
} |
|
68 |
} |
|
69 |
||
70 |
// process loop |
|
71 |
val process = |
|
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
72 |
ML_Process(options, logic = logic, args = List("-i"), |
62633 | 73 |
modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII"), |
74 |
store = Sessions.store(system_mode)) |
|
62559 | 75 |
val process_output = Future.thread[Unit]("process_output") { |
62561
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
76 |
try { |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
77 |
var result = new StringBuilder(100) |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
78 |
var finished = false |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
79 |
while (!finished) { |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
80 |
var c = -1 |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
81 |
var done = false |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
82 |
while (!done && (result.length == 0 || process.stdout.ready)) { |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
83 |
c = process.stdout.read |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
84 |
if (c >= 0) result.append(c.asInstanceOf[Char]) |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
85 |
else done = true |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
86 |
} |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
87 |
if (result.length > 0) { |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
88 |
System.out.print(result.toString) |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
89 |
System.out.flush() |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
90 |
result.length = 0 |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
91 |
} |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
92 |
else { |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
93 |
process.stdout.close() |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
94 |
finished = true |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
95 |
} |
62559 | 96 |
} |
97 |
} |
|
62561
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
98 |
catch { case e: IOException => case Exn.Interrupt() => } |
62559 | 99 |
} |
100 |
val process_input = Future.thread[Unit]("process_input") { |
|
62562
905a5db3932d
back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents:
62561
diff
changeset
|
101 |
val reader = new BufferedReader(new InputStreamReader(System.in)) |
62559 | 102 |
POSIX_Interrupt.handler { process.interrupt } { |
62561
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
103 |
try { |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
104 |
var finished = false |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
105 |
while (!finished) { |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
106 |
reader.readLine() match { |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
107 |
case null => |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
108 |
process.stdin.close() |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
109 |
finished = true |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
110 |
case line => |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
111 |
process.stdin.write(line) |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
112 |
process.stdin.write("\n") |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
113 |
process.stdin.flush() |
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
114 |
} |
62559 | 115 |
} |
116 |
} |
|
62561
4bf00f54e4bc
ignore execeptions that usually occur due to shutdown;
wenzelm
parents:
62559
diff
changeset
|
117 |
catch { case e: IOException => case Exn.Interrupt() => } |
62559 | 118 |
} |
119 |
} |
|
120 |
val process_result = Future.thread[Int]("process_result") { |
|
121 |
val rc = process.join |
|
122 |
process_input.cancel |
|
123 |
rc |
|
124 |
} |
|
125 |
||
126 |
process_output.join |
|
127 |
process_input.join |
|
62562
905a5db3932d
back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents:
62561
diff
changeset
|
128 |
process_result.join |
62559 | 129 |
} |
130 |
} |
|
131 |
} |