1 /* Title: Pure/Tools/ml_console.scala |
|
2 Author: Makarius |
|
3 |
|
4 The raw ML process in interactive mode. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 import java.io.{IOException, BufferedReader, InputStreamReader} |
|
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 raw_ml_system = false |
|
26 var system_mode = false |
|
27 |
|
28 val getopts = Getopts(""" |
|
29 Usage: isabelle console [OPTIONS] |
|
30 |
|
31 Options are: |
|
32 -d DIR include session directory |
|
33 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
|
34 -m MODE add print mode for output |
|
35 -n no build of session image on startup |
|
36 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
37 -r bootstrap from raw Poly/ML |
|
38 -s system build mode for session image |
|
39 |
|
40 Build a logic session image and run the raw Isabelle ML process |
|
41 in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" + |
|
42 quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """. |
|
43 """, |
|
44 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
|
45 "l:" -> (arg => logic = arg), |
|
46 "m:" -> (arg => modes = arg :: modes), |
|
47 "n" -> (arg => no_build = true), |
|
48 "o:" -> (arg => options = options + arg), |
|
49 "r" -> (_ => raw_ml_system = true), |
|
50 "s" -> (_ => system_mode = true)) |
|
51 |
|
52 val more_args = getopts(args) |
|
53 if (!more_args.isEmpty) getopts.usage() |
|
54 |
|
55 |
|
56 // build |
|
57 if (!no_build && !raw_ml_system && |
|
58 !Build.build(options = options, build_heap = true, no_build = true, |
|
59 dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok) |
|
60 { |
|
61 val progress = new Console_Progress() |
|
62 progress.echo("Build started for Isabelle/" + logic + " ...") |
|
63 progress.interrupt_handler { |
|
64 val res = |
|
65 Build.build(options = options, progress = progress, build_heap = true, |
|
66 dirs = dirs, system_mode = system_mode, sessions = List(logic)) |
|
67 if (!res.ok) sys.exit(res.rc) |
|
68 } |
|
69 } |
|
70 |
|
71 // process loop |
|
72 val process = |
|
73 ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true, |
|
74 modes = if (raw_ml_system) Nil else modes ::: List("ASCII"), |
|
75 raw_ml_system = raw_ml_system, store = Sessions.store(system_mode), |
|
76 session_base = |
|
77 if (raw_ml_system) None |
|
78 else Some(Sessions.session_base(options, logic, dirs))) |
|
79 val process_output = Future.thread[Unit]("process_output") { |
|
80 try { |
|
81 var result = new StringBuilder(100) |
|
82 var finished = false |
|
83 while (!finished) { |
|
84 var c = -1 |
|
85 var done = false |
|
86 while (!done && (result.length == 0 || process.stdout.ready)) { |
|
87 c = process.stdout.read |
|
88 if (c >= 0) result.append(c.asInstanceOf[Char]) |
|
89 else done = true |
|
90 } |
|
91 if (result.length > 0) { |
|
92 System.out.print(result.toString) |
|
93 System.out.flush() |
|
94 result.length = 0 |
|
95 } |
|
96 else { |
|
97 process.stdout.close() |
|
98 finished = true |
|
99 } |
|
100 } |
|
101 } |
|
102 catch { case e: IOException => case Exn.Interrupt() => } |
|
103 } |
|
104 val process_input = Future.thread[Unit]("process_input") { |
|
105 val reader = new BufferedReader(new InputStreamReader(System.in)) |
|
106 POSIX_Interrupt.handler { process.interrupt } { |
|
107 try { |
|
108 var finished = false |
|
109 while (!finished) { |
|
110 reader.readLine() match { |
|
111 case null => |
|
112 process.stdin.close() |
|
113 finished = true |
|
114 case line => |
|
115 process.stdin.write(line) |
|
116 process.stdin.write("\n") |
|
117 process.stdin.flush() |
|
118 } |
|
119 } |
|
120 } |
|
121 catch { case e: IOException => case Exn.Interrupt() => } |
|
122 } |
|
123 } |
|
124 val process_result = Future.thread[Int]("process_result") { |
|
125 val rc = process.join |
|
126 process_input.cancel |
|
127 rc |
|
128 } |
|
129 |
|
130 process_output.join |
|
131 process_input.join |
|
132 process_result.join |
|
133 } |
|
134 } |
|
135 } |
|