equal
deleted
inserted
replaced
114 |
114 |
115 /* demo constructor */ |
115 /* demo constructor */ |
116 |
116 |
117 def this(args: String*) = |
117 def this(args: String*) = |
118 this(new Isabelle_System, |
118 this(new Isabelle_System, |
119 new Actor { def act = loop { react { case res => Console.println(res) } } }.start, args: _*) |
119 actor { loop { react { case res => Console.println(res) } } }, args: _*) |
120 |
120 |
121 |
121 |
122 /* process information */ |
122 /* process information */ |
123 |
123 |
124 @volatile private var proc: Process = null |
124 @volatile private var proc: Process = null |
212 } |
212 } |
213 |
213 |
214 |
214 |
215 /* stdin */ |
215 /* stdin */ |
216 |
216 |
217 private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") { |
217 private class Stdin_Thread(out_stream: OutputStream) extends Thread("isabelle: stdin") { |
218 override def run() = { |
218 override def run() = { |
219 val writer = new BufferedWriter(new OutputStreamWriter(out_stream, Standard_System.charset)) |
219 val writer = new BufferedWriter(new OutputStreamWriter(out_stream, Standard_System.charset)) |
220 var finished = false |
220 var finished = false |
221 while (!finished) { |
221 while (!finished) { |
222 try { |
222 try { |
242 } |
242 } |
243 |
243 |
244 |
244 |
245 /* stdout */ |
245 /* stdout */ |
246 |
246 |
247 private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") { |
247 private class Stdout_Thread(in_stream: InputStream) extends Thread("isabelle: stdout") { |
248 override def run() = { |
248 override def run() = { |
249 val reader = new BufferedReader(new InputStreamReader(in_stream, Standard_System.charset)) |
249 val reader = new BufferedReader(new InputStreamReader(in_stream, Standard_System.charset)) |
250 var result = new StringBuilder(100) |
250 var result = new StringBuilder(100) |
251 |
251 |
252 var finished = false |
252 var finished = false |
280 } |
280 } |
281 |
281 |
282 |
282 |
283 /* messages */ |
283 /* messages */ |
284 |
284 |
285 private class MessageThread(fifo: String) extends Thread("isabelle: messages") |
285 private class Message_Thread(fifo: String) extends Thread("isabelle: messages") |
286 { |
286 { |
287 private class Protocol_Error(msg: String) extends Exception(msg) |
287 private class Protocol_Error(msg: String) extends Exception(msg) |
288 override def run() |
288 override def run() |
289 { |
289 { |
290 val stream = system.fifo_stream(fifo) |
290 val stream = system.fifo_stream(fifo) |
361 |
361 |
362 |
362 |
363 /** main **/ |
363 /** main **/ |
364 |
364 |
365 { |
365 { |
366 /* isabelle version */ |
|
367 |
|
368 { |
|
369 val (msg, rc) = system.isabelle_tool("version") |
|
370 if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg) |
|
371 put_result(Kind.SYSTEM, msg) |
|
372 } |
|
373 |
|
374 |
|
375 /* messages */ |
366 /* messages */ |
376 |
367 |
377 val message_fifo = system.mk_fifo() |
368 val message_fifo = system.mk_fifo() |
378 def rm_fifo() = system.rm_fifo(message_fifo) |
369 def rm_fifo() = system.rm_fifo(message_fifo) |
379 |
370 |
380 val message_thread = new MessageThread(message_fifo) |
371 val message_thread = new Message_Thread(message_fifo) |
381 message_thread.start |
372 message_thread.start |
382 |
373 |
383 |
374 |
384 /* exec process */ |
375 /* exec process */ |
385 |
376 |
394 } |
385 } |
395 |
386 |
396 |
387 |
397 /* stdin/stdout */ |
388 /* stdin/stdout */ |
398 |
389 |
399 new StdinThread(proc.getOutputStream).start |
390 new Stdin_Thread(proc.getOutputStream).start |
400 new StdoutThread(proc.getInputStream).start |
391 new Stdout_Thread(proc.getInputStream).start |
401 |
392 |
402 |
393 |
403 /* exit */ |
394 /* exit */ |
404 |
395 |
405 new Thread("isabelle: exit") { |
396 new Thread("isabelle: exit") { |
409 put_result(Kind.SYSTEM, "Exit thread terminated") |
400 put_result(Kind.SYSTEM, "Exit thread terminated") |
410 put_result(Kind.EXIT, rc.toString) |
401 put_result(Kind.EXIT, rc.toString) |
411 rm_fifo() |
402 rm_fifo() |
412 } |
403 } |
413 }.start |
404 }.start |
414 |
|
415 } |
405 } |
416 } |
406 } |