8 |
8 |
9 package isabelle |
9 package isabelle |
10 |
10 |
11 import java.util.Properties |
11 import java.util.Properties |
12 import java.util.concurrent.LinkedBlockingQueue |
12 import java.util.concurrent.LinkedBlockingQueue |
13 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, IOException} |
13 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, |
|
14 InputStream, OutputStream, FileInputStream, IOException} |
14 |
15 |
15 import isabelle.{Symbol, XML} |
16 import isabelle.{Symbol, XML} |
16 |
17 |
17 |
18 |
18 object IsabelleProcess { |
19 object IsabelleProcess { |
|
20 |
|
21 private val charset = "UTF-8" |
|
22 |
19 |
23 |
20 /* results */ |
24 /* results */ |
21 |
25 |
22 object Kind extends Enumeration { |
26 object Kind extends Enumeration { |
23 //{{{ values |
27 //{{{ values |
24 // Posix channels/events |
28 // Posix channels/events |
25 val STDIN = Value("STDIN") |
29 val STDIN = Value("STDIN") |
26 val STDOUT = Value("STDOUT") |
30 val STDOUT = Value("STDOUT") |
27 val STDERR = Value("STDERR") |
|
28 val SIGNAL = Value("SIGNAL") |
31 val SIGNAL = Value("SIGNAL") |
29 val EXIT = Value("EXIT") |
32 val EXIT = Value("EXIT") |
30 // Isabelle messages |
33 // Isabelle messages |
31 val WRITELN = Value("WRITELN") |
34 val WRITELN = Value("WRITELN") |
32 val PRIORITY = Value("PRIORITY") |
35 val PRIORITY = Value("PRIORITY") |
198 } |
202 } |
199 |
203 |
200 |
204 |
201 /* stdout */ |
205 /* stdout */ |
202 |
206 |
203 private class StdoutThread(reader: BufferedReader) extends Thread { |
207 private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") { |
204 override def run() = { |
208 override def run() = { |
205 var kind = Kind.STDOUT |
209 val reader = new BufferedReader(new InputStreamReader(in_stream, charset)) |
206 var props: Properties = null |
|
207 var result = new StringBuilder |
|
208 |
|
209 var finished = false |
|
210 while (!finished) { |
|
211 try { |
|
212 if (kind == Kind.STDOUT) { |
|
213 //{{{ Char mode |
|
214 var c = -1 |
|
215 var done = false |
|
216 while (!done && (result.length == 0 || reader.ready)) { |
|
217 c = reader.read |
|
218 if (c > 0 && c != 2) result.append(c.asInstanceOf[Char]) |
|
219 else done = true |
|
220 } |
|
221 if (result.length > 0) { |
|
222 put_result(kind, null, result.toString) |
|
223 result.length = 0 |
|
224 } |
|
225 if (c == -1) { |
|
226 reader.close |
|
227 finished = true |
|
228 try_close() |
|
229 } |
|
230 else if (c == 2) { |
|
231 reader.read match { |
|
232 case 'A' => kind = Kind.WRITELN |
|
233 case 'B' => kind = Kind.PRIORITY |
|
234 case 'C' => kind = Kind.TRACING |
|
235 case 'D' => kind = Kind.WARNING |
|
236 case 'E' => kind = Kind.ERROR |
|
237 case 'F' => kind = Kind.DEBUG |
|
238 case 'G' => kind = Kind.PROMPT |
|
239 case 'H' => kind = Kind.INIT |
|
240 case 'I' => kind = Kind.STATUS |
|
241 case _ => kind = Kind.STDOUT |
|
242 } |
|
243 props = null |
|
244 } |
|
245 //}}} |
|
246 } |
|
247 else { |
|
248 //{{{ Line mode |
|
249 val line = reader.readLine |
|
250 if (line == null) { |
|
251 reader.close |
|
252 finished = true |
|
253 try_close() |
|
254 } |
|
255 else { |
|
256 val len = line.length |
|
257 // property |
|
258 if (line.endsWith("\u0002,")) { |
|
259 val i = line.indexOf('=') |
|
260 if (i > 0) { |
|
261 val name = line.substring(0, i) |
|
262 val value = line.substring(i + 1, len - 2) |
|
263 if (props == null) props = new Properties |
|
264 if (!props.containsKey(name)) props.setProperty(name, value) |
|
265 } |
|
266 } |
|
267 // last text line |
|
268 else if (line.endsWith("\u0002.")) { |
|
269 result.append(line.substring(0, len - 2)) |
|
270 put_result(kind, props, result.toString) |
|
271 result.length = 0 |
|
272 kind = Kind.STDOUT |
|
273 } |
|
274 // text line |
|
275 else { |
|
276 result.append(line) |
|
277 result.append('\n') |
|
278 } |
|
279 } |
|
280 //}}} |
|
281 } |
|
282 } |
|
283 catch { |
|
284 case e: IOException => put_result(Kind.SYSTEM, null, "Stdout thread: " + e.getMessage) |
|
285 } |
|
286 } |
|
287 put_result(Kind.SYSTEM, null, "Stdout thread terminated") |
|
288 } |
|
289 } |
|
290 |
|
291 |
|
292 /* stderr */ |
|
293 |
|
294 private class StderrThread(reader: BufferedReader) extends Thread { |
|
295 override def run() = { |
|
296 var result = new StringBuilder(100) |
210 var result = new StringBuilder(100) |
297 |
211 |
298 var finished = false |
212 var finished = false |
299 while (!finished) { |
213 while (!finished) { |
300 try { |
214 try { |
301 //{{{ |
215 //{{{ |
302 var c = -1 |
216 var c = -1 |
303 var done = false |
217 var done = false |
304 while (!done && (result.length == 0 || reader.ready)) { |
218 while (!done && (result.length == 0 || reader.ready)) { |
305 c = reader.read |
219 c = reader.read |
306 if (c > 0) result.append(c.asInstanceOf[Char]) |
220 if (c >= 0) result.append(c.asInstanceOf[Char]) |
307 else done = true |
221 else done = true |
308 } |
222 } |
309 if (result.length > 0) { |
223 if (result.length > 0) { |
310 put_result(Kind.STDERR, null, result.toString) |
224 put_result(Kind.STDOUT, null, result.toString) |
311 result.length = 0 |
225 result.length = 0 |
312 } |
226 } |
313 else { |
227 else { |
314 reader.close |
228 reader.close |
315 finished = true |
229 finished = true |
316 try_close() |
230 try_close() |
317 } |
231 } |
318 //}}} |
232 //}}} |
319 } |
233 } |
320 catch { |
234 catch { |
321 case e: IOException => put_result(Kind.SYSTEM, null, "Stderr thread: " + e.getMessage) |
235 case e: IOException => put_result(Kind.SYSTEM, null, "Stdout thread: " + e.getMessage) |
322 } |
236 } |
323 } |
237 } |
324 put_result(Kind.SYSTEM, null, "Stderr thread terminated") |
238 put_result(Kind.SYSTEM, null, "Stdout thread terminated") |
325 } |
239 } |
326 } |
240 } |
327 |
241 |
328 |
242 |
329 /* exit */ |
243 /* messages */ |
330 |
244 |
331 private class ExitThread extends Thread { |
245 private class MessageThread(fifo: String) extends Thread("isabelle: messages") { |
332 override def run() = { |
246 override def run() = { |
333 val rc = proc.waitFor() |
247 val reader = new BufferedReader(new InputStreamReader(new FileInputStream(fifo), charset)) |
334 Thread.sleep(300) |
248 var kind: Kind.Value = null |
335 put_result(Kind.SYSTEM, null, "Exit thread terminated") |
249 var props: Properties = null |
336 put_result(Kind.EXIT, null, Integer.toString(rc)) |
250 var result = new StringBuilder |
337 } |
251 |
338 } |
252 var finished = false |
339 |
253 while (!finished) { |
|
254 try { |
|
255 try { |
|
256 if (kind == null) { |
|
257 //{{{ Char mode -- resync |
|
258 var c = -1 |
|
259 do { |
|
260 c = reader.read |
|
261 if (c >= 0 && c != 2) result.append(c.asInstanceOf[Char]) |
|
262 } while (c >= 0 && c != 2) |
|
263 |
|
264 if (result.length > 0) { |
|
265 put_result(Kind.SYSTEM, null, "Malformed message:\n" + result.toString) |
|
266 result.length = 0 |
|
267 } |
|
268 if (c < 0) { |
|
269 reader.close |
|
270 finished = true |
|
271 try_close() |
|
272 } |
|
273 else { |
|
274 reader.read match { |
|
275 case 'A' => kind = Kind.WRITELN |
|
276 case 'B' => kind = Kind.PRIORITY |
|
277 case 'C' => kind = Kind.TRACING |
|
278 case 'D' => kind = Kind.WARNING |
|
279 case 'E' => kind = Kind.ERROR |
|
280 case 'F' => kind = Kind.DEBUG |
|
281 case 'G' => kind = Kind.PROMPT |
|
282 case 'H' => kind = Kind.INIT |
|
283 case 'I' => kind = Kind.STATUS |
|
284 case _ => kind = null |
|
285 } |
|
286 props = null |
|
287 } |
|
288 //}}} |
|
289 } |
|
290 else { |
|
291 //{{{ Line mode |
|
292 val line = reader.readLine |
|
293 if (line == null) { |
|
294 reader.close |
|
295 finished = true |
|
296 try_close() |
|
297 } |
|
298 else { |
|
299 val len = line.length |
|
300 // property |
|
301 if (line.endsWith("\u0002,")) { |
|
302 val i = line.indexOf('=') |
|
303 if (i > 0) { |
|
304 val name = line.substring(0, i) |
|
305 val value = line.substring(i + 1, len - 2) |
|
306 if (props == null) props = new Properties |
|
307 if (!props.containsKey(name)) props.setProperty(name, value) |
|
308 } |
|
309 } |
|
310 // last text line |
|
311 else if (line.endsWith("\u0002.")) { |
|
312 result.append(line.substring(0, len - 2)) |
|
313 put_result(kind, props, result.toString) |
|
314 result.length = 0 |
|
315 kind = null |
|
316 } |
|
317 // text line |
|
318 else { |
|
319 result.append(line) |
|
320 result.append('\n') |
|
321 } |
|
322 } |
|
323 //}}} |
|
324 } |
|
325 } |
|
326 catch { |
|
327 case e: IOException => put_result(Kind.SYSTEM, null, "Message thread: " + e.getMessage) |
|
328 } |
|
329 } |
|
330 catch { case _: InterruptedException => finished = true } |
|
331 } |
|
332 try { put_result(Kind.SYSTEM, null, "Message thread terminated") } |
|
333 catch { case _ : InterruptedException => } |
|
334 } |
|
335 } |
340 |
336 |
341 |
337 |
342 /** main **/ |
338 /** main **/ |
343 |
339 |
344 { |
340 { |
|
341 |
|
342 /* message fifo */ |
|
343 |
|
344 val fifo = |
|
345 try { |
|
346 val mkfifo = IsabelleSystem.exec(List(IsabelleSystem.getenv_strict("ISATOOL"), "mkfifo")) |
|
347 val fifo = new BufferedReader(new InputStreamReader(mkfifo.getInputStream, charset)).readLine |
|
348 if (mkfifo.waitFor == 0) fifo |
|
349 else error("Failed to create message fifo") |
|
350 } |
|
351 catch { |
|
352 case e: IOException => error("Failed to create message fifo: " + e.getMessage) |
|
353 } |
|
354 |
|
355 val message_thread = new MessageThread(fifo) |
|
356 |
|
357 |
345 /* exec process */ |
358 /* exec process */ |
346 |
359 |
347 try { |
360 try { |
348 proc = IsabelleSystem.exec(List( |
361 proc = IsabelleSystem.exec2(List( |
349 IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W") ++ args) |
362 IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W", fifo) ++ args) |
350 } |
363 } |
351 catch { |
364 catch { |
352 case e: IOException => error("Failed to execute Isabelle process: " + e.getMessage) |
365 case e: IOException => error("Failed to execute Isabelle process: " + e.getMessage) |
353 } |
366 } |
354 |
367 |
355 |
368 |
356 /* control process via threads */ |
369 /* stdin/stdout */ |
357 |
370 |
358 val charset = "UTF-8" |
371 new StdinThread(proc.getOutputStream).start |
359 new StdinThread(new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, charset))).start |
372 new StdoutThread(proc.getInputStream).start |
360 new StdoutThread(new BufferedReader(new InputStreamReader(proc.getInputStream, charset))).start |
373 |
361 new StderrThread(new BufferedReader(new InputStreamReader(proc.getErrorStream, charset))).start |
374 |
|
375 /* exit */ |
|
376 |
|
377 class ExitThread extends Thread("isabelle: exit") { |
|
378 override def run() = { |
|
379 val rc = proc.waitFor() |
|
380 Thread.sleep(300) |
|
381 put_result(Kind.SYSTEM, null, "Exit thread terminated") |
|
382 put_result(Kind.EXIT, null, Integer.toString(rc)) |
|
383 message_thread.interrupt |
|
384 } |
|
385 } |
|
386 message_thread.start |
362 new ExitThread().start |
387 new ExitThread().start |
363 } |
388 } |
364 |
389 |
365 } |
390 } |