wenzelm@30174
|
1 |
/* Title: Pure/System/isabelle_process.ML
|
wenzelm@27949
|
2 |
Author: Makarius
|
wenzelm@27963
|
3 |
Options: :folding=explicit:collapseFolds=1:
|
wenzelm@27949
|
4 |
|
wenzelm@27949
|
5 |
Isabelle process management -- always reactive due to multi-threaded I/O.
|
wenzelm@27949
|
6 |
*/
|
wenzelm@27949
|
7 |
|
wenzelm@27949
|
8 |
package isabelle
|
wenzelm@27949
|
9 |
|
wenzelm@27955
|
10 |
import java.util.concurrent.LinkedBlockingQueue
|
wenzelm@28045
|
11 |
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
|
wenzelm@28056
|
12 |
InputStream, OutputStream, IOException}
|
wenzelm@27949
|
13 |
|
wenzelm@27949
|
14 |
|
wenzelm@27973
|
15 |
object IsabelleProcess {
|
wenzelm@27973
|
16 |
|
wenzelm@27949
|
17 |
/* results */
|
wenzelm@27949
|
18 |
|
wenzelm@27949
|
19 |
object Kind extends Enumeration {
|
wenzelm@28344
|
20 |
//{{{ values and codes
|
wenzelm@28344
|
21 |
// internal system notification
|
wenzelm@28344
|
22 |
val SYSTEM = Value("SYSTEM")
|
wenzelm@27949
|
23 |
// Posix channels/events
|
wenzelm@27949
|
24 |
val STDIN = Value("STDIN")
|
wenzelm@27949
|
25 |
val STDOUT = Value("STDOUT")
|
wenzelm@27949
|
26 |
val SIGNAL = Value("SIGNAL")
|
wenzelm@27949
|
27 |
val EXIT = Value("EXIT")
|
wenzelm@27949
|
28 |
// Isabelle messages
|
wenzelm@28344
|
29 |
val INIT = Value("INIT")
|
wenzelm@28344
|
30 |
val STATUS = Value("STATUS")
|
wenzelm@27949
|
31 |
val WRITELN = Value("WRITELN")
|
wenzelm@27949
|
32 |
val PRIORITY = Value("PRIORITY")
|
wenzelm@27949
|
33 |
val TRACING = Value("TRACING")
|
wenzelm@27949
|
34 |
val WARNING = Value("WARNING")
|
wenzelm@27949
|
35 |
val ERROR = Value("ERROR")
|
wenzelm@27949
|
36 |
val DEBUG = Value("DEBUG")
|
wenzelm@28344
|
37 |
// messages codes
|
wenzelm@28344
|
38 |
val code = Map(
|
wenzelm@28344
|
39 |
('A' : Int) -> Kind.INIT,
|
wenzelm@28344
|
40 |
('B' : Int) -> Kind.STATUS,
|
wenzelm@28344
|
41 |
('C' : Int) -> Kind.WRITELN,
|
wenzelm@28344
|
42 |
('D' : Int) -> Kind.PRIORITY,
|
wenzelm@28344
|
43 |
('E' : Int) -> Kind.TRACING,
|
wenzelm@28344
|
44 |
('F' : Int) -> Kind.WARNING,
|
wenzelm@28344
|
45 |
('G' : Int) -> Kind.ERROR,
|
wenzelm@28344
|
46 |
('H' : Int) -> Kind.DEBUG,
|
wenzelm@28344
|
47 |
('0' : Int) -> Kind.SYSTEM,
|
wenzelm@28344
|
48 |
('1' : Int) -> Kind.STDIN,
|
wenzelm@28344
|
49 |
('2' : Int) -> Kind.STDOUT,
|
wenzelm@28344
|
50 |
('3' : Int) -> Kind.SIGNAL,
|
wenzelm@28344
|
51 |
('4' : Int) -> Kind.EXIT)
|
wenzelm@29522
|
52 |
// message markup
|
wenzelm@29522
|
53 |
val markup = Map(
|
wenzelm@29522
|
54 |
Kind.INIT -> Markup.INIT,
|
wenzelm@29522
|
55 |
Kind.STATUS -> Markup.STATUS,
|
wenzelm@29522
|
56 |
Kind.WRITELN -> Markup.WRITELN,
|
wenzelm@29522
|
57 |
Kind.PRIORITY -> Markup.PRIORITY,
|
wenzelm@29522
|
58 |
Kind.TRACING -> Markup.TRACING,
|
wenzelm@29522
|
59 |
Kind.WARNING -> Markup.WARNING,
|
wenzelm@29522
|
60 |
Kind.ERROR -> Markup.ERROR,
|
wenzelm@29522
|
61 |
Kind.DEBUG -> Markup.DEBUG,
|
wenzelm@29522
|
62 |
Kind.SYSTEM -> Markup.SYSTEM,
|
wenzelm@29522
|
63 |
Kind.STDIN -> Markup.STDIN,
|
wenzelm@29522
|
64 |
Kind.STDOUT -> Markup.STDOUT,
|
wenzelm@29522
|
65 |
Kind.SIGNAL -> Markup.SIGNAL,
|
wenzelm@29522
|
66 |
Kind.EXIT -> Markup.EXIT)
|
wenzelm@27949
|
67 |
//}}}
|
wenzelm@27949
|
68 |
def is_raw(kind: Value) =
|
wenzelm@28045
|
69 |
kind == STDOUT
|
wenzelm@27990
|
70 |
def is_control(kind: Value) =
|
wenzelm@28344
|
71 |
kind == SYSTEM ||
|
wenzelm@27990
|
72 |
kind == SIGNAL ||
|
wenzelm@28344
|
73 |
kind == EXIT
|
wenzelm@27949
|
74 |
def is_system(kind: Value) =
|
wenzelm@28344
|
75 |
kind == SYSTEM ||
|
wenzelm@27949
|
76 |
kind == STDIN ||
|
wenzelm@27949
|
77 |
kind == SIGNAL ||
|
wenzelm@27949
|
78 |
kind == EXIT ||
|
wenzelm@28498
|
79 |
kind == STATUS
|
wenzelm@27949
|
80 |
}
|
wenzelm@27949
|
81 |
|
wenzelm@29572
|
82 |
class Result(val kind: Kind.Value, val props: List[(String, String)], val result: String) {
|
wenzelm@27949
|
83 |
override def toString = {
|
wenzelm@29522
|
84 |
val trees = YXML.parse_body_failsafe(result)
|
wenzelm@29522
|
85 |
val res =
|
wenzelm@29522
|
86 |
if (kind == Kind.STATUS) trees.map(_.toString).mkString
|
wenzelm@29522
|
87 |
else trees.flatMap(XML.content(_).mkString).mkString
|
wenzelm@29572
|
88 |
if (props.isEmpty)
|
wenzelm@29572
|
89 |
kind.toString + " [[" + res + "]]"
|
wenzelm@29572
|
90 |
else
|
wenzelm@29572
|
91 |
kind.toString + " " +
|
wenzelm@29572
|
92 |
(for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
|
wenzelm@27949
|
93 |
}
|
wenzelm@29192
|
94 |
def is_raw = Kind.is_raw(kind)
|
wenzelm@29192
|
95 |
def is_control = Kind.is_control(kind)
|
wenzelm@29192
|
96 |
def is_system = Kind.is_system(kind)
|
wenzelm@27973
|
97 |
}
|
wenzelm@27949
|
98 |
|
wenzelm@29572
|
99 |
def parse_message(isabelle_system: IsabelleSystem, result: Result) =
|
wenzelm@29572
|
100 |
{
|
wenzelm@29572
|
101 |
XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
|
wenzelm@29572
|
102 |
YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
|
wenzelm@29522
|
103 |
}
|
wenzelm@27973
|
104 |
}
|
wenzelm@27973
|
105 |
|
wenzelm@27973
|
106 |
|
wenzelm@29192
|
107 |
class IsabelleProcess(isabelle_system: IsabelleSystem,
|
wenzelm@29192
|
108 |
results: EventBus[IsabelleProcess.Result], args: String*)
|
wenzelm@29192
|
109 |
{
|
wenzelm@29192
|
110 |
import IsabelleProcess._
|
wenzelm@29194
|
111 |
|
wenzelm@27973
|
112 |
|
wenzelm@29192
|
113 |
/* demo constructor */
|
wenzelm@27973
|
114 |
|
wenzelm@29192
|
115 |
def this(args: String*) =
|
wenzelm@29196
|
116 |
this(new IsabelleSystem, new EventBus[IsabelleProcess.Result] + Console.println, args: _*)
|
wenzelm@29174
|
117 |
|
wenzelm@29174
|
118 |
|
wenzelm@27973
|
119 |
/* process information */
|
wenzelm@27973
|
120 |
|
wenzelm@29648
|
121 |
@volatile private var proc: Process = null
|
wenzelm@29648
|
122 |
@volatile private var closing = false
|
wenzelm@29648
|
123 |
@volatile private var pid: String = null
|
wenzelm@29648
|
124 |
@volatile private var the_session: String = null
|
wenzelm@29572
|
125 |
def session = the_session
|
wenzelm@27973
|
126 |
|
wenzelm@27973
|
127 |
|
wenzelm@27973
|
128 |
/* results */
|
wenzelm@27949
|
129 |
|
wenzelm@29572
|
130 |
def parse_message(result: Result): XML.Tree =
|
wenzelm@29572
|
131 |
IsabelleProcess.parse_message(isabelle_system, result)
|
wenzelm@29572
|
132 |
|
wenzelm@29192
|
133 |
private val result_queue = new LinkedBlockingQueue[Result]
|
wenzelm@27949
|
134 |
|
wenzelm@29572
|
135 |
private def put_result(kind: Kind.Value, props: List[(String, String)], result: String)
|
wenzelm@29572
|
136 |
{
|
wenzelm@29572
|
137 |
if (kind == Kind.INIT) {
|
wenzelm@29572
|
138 |
val map = Map(props: _*)
|
wenzelm@29572
|
139 |
if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
|
wenzelm@29572
|
140 |
if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
|
wenzelm@27963
|
141 |
}
|
wenzelm@29192
|
142 |
result_queue.put(new Result(kind, props, result))
|
wenzelm@27949
|
143 |
}
|
wenzelm@27949
|
144 |
|
wenzelm@29192
|
145 |
private class ResultThread extends Thread("isabelle: results") {
|
wenzelm@29192
|
146 |
override def run() = {
|
wenzelm@29192
|
147 |
var finished = false
|
wenzelm@29192
|
148 |
while (!finished) {
|
wenzelm@29192
|
149 |
val result =
|
wenzelm@29192
|
150 |
try { result_queue.take }
|
wenzelm@29192
|
151 |
catch { case _: NullPointerException => null }
|
wenzelm@27973
|
152 |
|
wenzelm@29192
|
153 |
if (result != null) {
|
wenzelm@29572
|
154 |
results.event(result)
|
wenzelm@29192
|
155 |
if (result.kind == Kind.EXIT) finished = true
|
wenzelm@29192
|
156 |
}
|
wenzelm@29192
|
157 |
else finished = true
|
wenzelm@29192
|
158 |
}
|
wenzelm@29192
|
159 |
}
|
wenzelm@27992
|
160 |
}
|
wenzelm@27992
|
161 |
|
wenzelm@27973
|
162 |
|
wenzelm@27973
|
163 |
/* signals */
|
wenzelm@27973
|
164 |
|
wenzelm@27973
|
165 |
def interrupt() = synchronized {
|
wenzelm@27993
|
166 |
if (proc == null) error("Cannot interrupt Isabelle: no process")
|
wenzelm@29572
|
167 |
if (pid == null) put_result(Kind.SYSTEM, Nil, "Cannot interrupt: unknown pid")
|
wenzelm@27973
|
168 |
else {
|
wenzelm@27973
|
169 |
try {
|
wenzelm@29178
|
170 |
if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0)
|
wenzelm@29572
|
171 |
put_result(Kind.SIGNAL, Nil, "INT")
|
wenzelm@27990
|
172 |
else
|
wenzelm@29572
|
173 |
put_result(Kind.SYSTEM, Nil, "Cannot interrupt: kill command failed")
|
wenzelm@27973
|
174 |
}
|
wenzelm@27993
|
175 |
catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
|
wenzelm@27973
|
176 |
}
|
wenzelm@27973
|
177 |
}
|
wenzelm@27973
|
178 |
|
wenzelm@27973
|
179 |
def kill() = synchronized {
|
wenzelm@27993
|
180 |
if (proc == 0) error("Cannot kill Isabelle: no process")
|
wenzelm@27973
|
181 |
else {
|
wenzelm@27973
|
182 |
try_close()
|
wenzelm@27990
|
183 |
Thread.sleep(500)
|
wenzelm@29572
|
184 |
put_result(Kind.SIGNAL, Nil, "KILL")
|
wenzelm@27973
|
185 |
proc.destroy
|
wenzelm@27973
|
186 |
proc = null
|
wenzelm@27990
|
187 |
pid = null
|
wenzelm@27973
|
188 |
}
|
wenzelm@27973
|
189 |
}
|
wenzelm@27973
|
190 |
|
wenzelm@27949
|
191 |
|
wenzelm@27949
|
192 |
/* output being piped into the process */
|
wenzelm@27949
|
193 |
|
wenzelm@27990
|
194 |
private val output = new LinkedBlockingQueue[String]
|
wenzelm@27949
|
195 |
|
wenzelm@28045
|
196 |
private def output_raw(text: String) = synchronized {
|
wenzelm@27993
|
197 |
if (proc == null) error("Cannot output to Isabelle: no process")
|
wenzelm@27993
|
198 |
if (closing) error("Cannot output to Isabelle: already closing")
|
wenzelm@27955
|
199 |
output.put(text)
|
wenzelm@27949
|
200 |
}
|
wenzelm@27949
|
201 |
|
wenzelm@28303
|
202 |
def output_sync(text: String) =
|
wenzelm@28045
|
203 |
output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
|
wenzelm@27949
|
204 |
|
wenzelm@27963
|
205 |
|
wenzelm@27963
|
206 |
def command(text: String) =
|
wenzelm@27949
|
207 |
output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text))
|
wenzelm@27949
|
208 |
|
wenzelm@29572
|
209 |
def command(props: List[(String, String)], text: String) =
|
wenzelm@27949
|
210 |
output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " +
|
wenzelm@27949
|
211 |
IsabelleSyntax.encode_string(text))
|
wenzelm@27949
|
212 |
|
wenzelm@27963
|
213 |
def ML(text: String) =
|
wenzelm@27949
|
214 |
output_sync("ML_val " + IsabelleSyntax.encode_string(text))
|
wenzelm@27949
|
215 |
|
wenzelm@27949
|
216 |
def close() = synchronized { // FIXME watchdog/timeout
|
wenzelm@27949
|
217 |
output_raw("\u0000")
|
wenzelm@27949
|
218 |
closing = true
|
wenzelm@27949
|
219 |
}
|
wenzelm@27949
|
220 |
|
wenzelm@27949
|
221 |
def try_close() = synchronized {
|
wenzelm@27949
|
222 |
if (proc != null && !closing) {
|
wenzelm@27949
|
223 |
try { close() }
|
wenzelm@27993
|
224 |
catch { case _: RuntimeException => }
|
wenzelm@27949
|
225 |
}
|
wenzelm@27949
|
226 |
}
|
wenzelm@27949
|
227 |
|
wenzelm@27949
|
228 |
|
wenzelm@27949
|
229 |
/* stdin */
|
wenzelm@27949
|
230 |
|
wenzelm@28045
|
231 |
private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
|
wenzelm@27949
|
232 |
override def run() = {
|
wenzelm@29174
|
233 |
val writer = new BufferedWriter(new OutputStreamWriter(out_stream, isabelle_system.charset))
|
wenzelm@27949
|
234 |
var finished = false
|
wenzelm@27949
|
235 |
while (!finished) {
|
wenzelm@27949
|
236 |
try {
|
wenzelm@27949
|
237 |
//{{{
|
wenzelm@27955
|
238 |
val s = output.take
|
wenzelm@27949
|
239 |
if (s == "\u0000") {
|
wenzelm@27949
|
240 |
writer.close
|
wenzelm@27949
|
241 |
finished = true
|
wenzelm@27949
|
242 |
}
|
wenzelm@27949
|
243 |
else {
|
wenzelm@29572
|
244 |
put_result(Kind.STDIN, Nil, s)
|
wenzelm@27949
|
245 |
writer.write(s)
|
wenzelm@27949
|
246 |
writer.flush
|
wenzelm@27949
|
247 |
}
|
wenzelm@27949
|
248 |
//}}}
|
wenzelm@27949
|
249 |
}
|
wenzelm@27949
|
250 |
catch {
|
wenzelm@29572
|
251 |
case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdin thread: " + e.getMessage)
|
wenzelm@27949
|
252 |
}
|
wenzelm@27949
|
253 |
}
|
wenzelm@29572
|
254 |
put_result(Kind.SYSTEM, Nil, "Stdin thread terminated")
|
wenzelm@27949
|
255 |
}
|
wenzelm@27949
|
256 |
}
|
wenzelm@27949
|
257 |
|
wenzelm@27949
|
258 |
|
wenzelm@27949
|
259 |
/* stdout */
|
wenzelm@27949
|
260 |
|
wenzelm@28045
|
261 |
private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
|
wenzelm@27949
|
262 |
override def run() = {
|
wenzelm@29174
|
263 |
val reader = new BufferedReader(new InputStreamReader(in_stream, isabelle_system.charset))
|
wenzelm@27949
|
264 |
var result = new StringBuilder(100)
|
wenzelm@27949
|
265 |
|
wenzelm@27949
|
266 |
var finished = false
|
wenzelm@27949
|
267 |
while (!finished) {
|
wenzelm@27949
|
268 |
try {
|
wenzelm@27949
|
269 |
//{{{
|
wenzelm@27949
|
270 |
var c = -1
|
wenzelm@27949
|
271 |
var done = false
|
wenzelm@27949
|
272 |
while (!done && (result.length == 0 || reader.ready)) {
|
wenzelm@27949
|
273 |
c = reader.read
|
wenzelm@28045
|
274 |
if (c >= 0) result.append(c.asInstanceOf[Char])
|
wenzelm@27949
|
275 |
else done = true
|
wenzelm@27949
|
276 |
}
|
wenzelm@27949
|
277 |
if (result.length > 0) {
|
wenzelm@29572
|
278 |
put_result(Kind.STDOUT, Nil, result.toString)
|
wenzelm@27949
|
279 |
result.length = 0
|
wenzelm@27949
|
280 |
}
|
wenzelm@27949
|
281 |
else {
|
wenzelm@27949
|
282 |
reader.close
|
wenzelm@27949
|
283 |
finished = true
|
wenzelm@27949
|
284 |
try_close()
|
wenzelm@27949
|
285 |
}
|
wenzelm@27949
|
286 |
//}}}
|
wenzelm@27963
|
287 |
}
|
wenzelm@27963
|
288 |
catch {
|
wenzelm@29572
|
289 |
case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdout thread: " + e.getMessage)
|
wenzelm@27949
|
290 |
}
|
wenzelm@27949
|
291 |
}
|
wenzelm@29572
|
292 |
put_result(Kind.SYSTEM, Nil, "Stdout thread terminated")
|
wenzelm@27949
|
293 |
}
|
wenzelm@27949
|
294 |
}
|
wenzelm@27949
|
295 |
|
wenzelm@27949
|
296 |
|
wenzelm@28045
|
297 |
/* messages */
|
wenzelm@27949
|
298 |
|
wenzelm@28045
|
299 |
private class MessageThread(fifo: String) extends Thread("isabelle: messages") {
|
wenzelm@27949
|
300 |
override def run() = {
|
wenzelm@29174
|
301 |
val reader = isabelle_system.fifo_reader(fifo)
|
wenzelm@28045
|
302 |
var kind: Kind.Value = null
|
wenzelm@29572
|
303 |
var props: List[(String, String)] = Nil
|
wenzelm@28045
|
304 |
var result = new StringBuilder
|
wenzelm@28045
|
305 |
|
wenzelm@28045
|
306 |
var finished = false
|
wenzelm@28045
|
307 |
while (!finished) {
|
wenzelm@28045
|
308 |
try {
|
wenzelm@28063
|
309 |
if (kind == null) {
|
wenzelm@28063
|
310 |
//{{{ Char mode -- resync
|
wenzelm@28063
|
311 |
var c = -1
|
wenzelm@28063
|
312 |
do {
|
wenzelm@28063
|
313 |
c = reader.read
|
wenzelm@28063
|
314 |
if (c >= 0 && c != 2) result.append(c.asInstanceOf[Char])
|
wenzelm@28063
|
315 |
} while (c >= 0 && c != 2)
|
wenzelm@28063
|
316 |
|
wenzelm@28063
|
317 |
if (result.length > 0) {
|
wenzelm@29572
|
318 |
put_result(Kind.SYSTEM, Nil, "Malformed message:\n" + result.toString)
|
wenzelm@28063
|
319 |
result.length = 0
|
wenzelm@28063
|
320 |
}
|
wenzelm@28063
|
321 |
if (c < 0) {
|
wenzelm@28063
|
322 |
reader.close
|
wenzelm@28063
|
323 |
finished = true
|
wenzelm@28063
|
324 |
try_close()
|
wenzelm@28045
|
325 |
}
|
wenzelm@28045
|
326 |
else {
|
wenzelm@28344
|
327 |
c = reader.read
|
wenzelm@28344
|
328 |
if (Kind.code.isDefinedAt(c)) kind = Kind.code(c)
|
wenzelm@28344
|
329 |
else kind = null
|
wenzelm@28063
|
330 |
}
|
wenzelm@28063
|
331 |
//}}}
|
wenzelm@28063
|
332 |
}
|
wenzelm@28063
|
333 |
else {
|
wenzelm@28063
|
334 |
//{{{ Line mode
|
wenzelm@28063
|
335 |
val line = reader.readLine
|
wenzelm@28063
|
336 |
if (line == null) {
|
wenzelm@28063
|
337 |
reader.close
|
wenzelm@28063
|
338 |
finished = true
|
wenzelm@28063
|
339 |
try_close()
|
wenzelm@28063
|
340 |
}
|
wenzelm@28063
|
341 |
else {
|
wenzelm@28063
|
342 |
val len = line.length
|
wenzelm@28063
|
343 |
// property
|
wenzelm@28063
|
344 |
if (line.endsWith("\u0002,")) {
|
wenzelm@28063
|
345 |
val i = line.indexOf('=')
|
wenzelm@28063
|
346 |
if (i > 0) {
|
wenzelm@28063
|
347 |
val name = line.substring(0, i)
|
wenzelm@28063
|
348 |
val value = line.substring(i + 1, len - 2)
|
wenzelm@29572
|
349 |
props = (name, value) :: props
|
wenzelm@28045
|
350 |
}
|
wenzelm@28045
|
351 |
}
|
wenzelm@28063
|
352 |
// last text line
|
wenzelm@28063
|
353 |
else if (line.endsWith("\u0002.")) {
|
wenzelm@28063
|
354 |
result.append(line.substring(0, len - 2))
|
wenzelm@29572
|
355 |
put_result(kind, props.reverse, result.toString)
|
wenzelm@29573
|
356 |
kind = null
|
wenzelm@29573
|
357 |
props = Nil
|
wenzelm@28063
|
358 |
result.length = 0
|
wenzelm@28063
|
359 |
}
|
wenzelm@28063
|
360 |
// text line
|
wenzelm@28063
|
361 |
else {
|
wenzelm@28063
|
362 |
result.append(line)
|
wenzelm@28063
|
363 |
result.append('\n')
|
wenzelm@28063
|
364 |
}
|
wenzelm@28045
|
365 |
}
|
wenzelm@28063
|
366 |
//}}}
|
wenzelm@28045
|
367 |
}
|
wenzelm@28045
|
368 |
}
|
wenzelm@28063
|
369 |
catch {
|
wenzelm@29572
|
370 |
case e: IOException => put_result(Kind.SYSTEM, Nil, "Message thread: " + e.getMessage)
|
wenzelm@28063
|
371 |
}
|
wenzelm@28045
|
372 |
}
|
wenzelm@29572
|
373 |
put_result(Kind.SYSTEM, Nil, "Message thread terminated")
|
wenzelm@27949
|
374 |
}
|
wenzelm@27949
|
375 |
}
|
wenzelm@27949
|
376 |
|
wenzelm@27949
|
377 |
|
wenzelm@29192
|
378 |
|
wenzelm@27949
|
379 |
/** main **/
|
wenzelm@27949
|
380 |
|
wenzelm@27949
|
381 |
{
|
wenzelm@28497
|
382 |
/* isabelle version */
|
wenzelm@28497
|
383 |
|
wenzelm@28497
|
384 |
{
|
wenzelm@29174
|
385 |
val (msg, rc) = isabelle_system.isabelle_tool("version")
|
wenzelm@28497
|
386 |
if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
|
wenzelm@29572
|
387 |
put_result(Kind.SYSTEM, Nil, msg)
|
wenzelm@28497
|
388 |
}
|
wenzelm@28497
|
389 |
|
wenzelm@28045
|
390 |
|
wenzelm@29192
|
391 |
/* messages */
|
wenzelm@28045
|
392 |
|
wenzelm@29174
|
393 |
val message_fifo = isabelle_system.mk_fifo()
|
wenzelm@29174
|
394 |
def rm_fifo() = isabelle_system.rm_fifo(message_fifo)
|
wenzelm@28045
|
395 |
|
wenzelm@28063
|
396 |
val message_thread = new MessageThread(message_fifo)
|
wenzelm@28063
|
397 |
message_thread.start
|
wenzelm@28045
|
398 |
|
wenzelm@29194
|
399 |
new ResultThread().start
|
wenzelm@29194
|
400 |
|
wenzelm@28045
|
401 |
|
wenzelm@27973
|
402 |
/* exec process */
|
wenzelm@27949
|
403 |
|
wenzelm@27973
|
404 |
try {
|
wenzelm@28501
|
405 |
val cmdline =
|
wenzelm@29174
|
406 |
List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
|
wenzelm@29178
|
407 |
proc = isabelle_system.execute(true, cmdline: _*)
|
wenzelm@27973
|
408 |
}
|
wenzelm@27993
|
409 |
catch {
|
wenzelm@28063
|
410 |
case e: IOException =>
|
wenzelm@28063
|
411 |
rm_fifo()
|
wenzelm@28063
|
412 |
error("Failed to execute Isabelle process: " + e.getMessage)
|
wenzelm@27993
|
413 |
}
|
wenzelm@27963
|
414 |
|
wenzelm@27949
|
415 |
|
wenzelm@28045
|
416 |
/* stdin/stdout */
|
wenzelm@27949
|
417 |
|
wenzelm@28045
|
418 |
new StdinThread(proc.getOutputStream).start
|
wenzelm@28045
|
419 |
new StdoutThread(proc.getInputStream).start
|
wenzelm@28045
|
420 |
|
wenzelm@28045
|
421 |
|
wenzelm@28045
|
422 |
/* exit */
|
wenzelm@28045
|
423 |
|
wenzelm@28063
|
424 |
new Thread("isabelle: exit") {
|
wenzelm@28045
|
425 |
override def run() = {
|
wenzelm@28045
|
426 |
val rc = proc.waitFor()
|
wenzelm@28045
|
427 |
Thread.sleep(300)
|
wenzelm@29572
|
428 |
put_result(Kind.SYSTEM, Nil, "Exit thread terminated")
|
wenzelm@29572
|
429 |
put_result(Kind.EXIT, Nil, Integer.toString(rc))
|
wenzelm@28063
|
430 |
rm_fifo()
|
wenzelm@28045
|
431 |
}
|
wenzelm@28063
|
432 |
}.start
|
wenzelm@28063
|
433 |
|
wenzelm@27949
|
434 |
}
|
wenzelm@27949
|
435 |
}
|