equal
deleted
inserted
replaced
145 |
145 |
146 |
146 |
147 |
147 |
148 /** stream actors **/ |
148 /** stream actors **/ |
149 |
149 |
150 private val in_fifo = system.mk_fifo() |
|
151 private val out_fifo = system.mk_fifo() |
|
152 private def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) } |
|
153 |
|
154 private case class Input_Text(text: String) |
150 private case class Input_Text(text: String) |
155 private case class Input_Chunks(chunks: List[Array[Byte]]) |
151 private case class Input_Chunks(chunks: List[Array[Byte]]) |
156 private case object Close |
152 private case object Close |
157 |
153 |
158 |
154 |
222 } |
218 } |
223 |
219 |
224 |
220 |
225 /* command input */ |
221 /* command input */ |
226 |
222 |
227 private def input_actor(name: String): Actor = |
223 private def input_actor(name: String, fifo: String): Actor = |
228 Simple_Thread.actor(name) { |
224 Simple_Thread.actor(name) { |
229 val stream = new BufferedOutputStream(system.fifo_output_stream(in_fifo)) // FIXME potentially blocking forever |
225 val stream = new BufferedOutputStream(system.fifo_output_stream(fifo)) // FIXME potentially blocking forever |
230 var finished = false |
226 var finished = false |
231 while (!finished) { |
227 while (!finished) { |
232 try { |
228 try { |
233 //{{{ |
229 //{{{ |
234 receive { |
230 receive { |
254 |
250 |
255 /* message output */ |
251 /* message output */ |
256 |
252 |
257 private class Protocol_Error(msg: String) extends Exception(msg) |
253 private class Protocol_Error(msg: String) extends Exception(msg) |
258 |
254 |
259 private def message_actor(name: String): Actor = |
255 private def message_actor(name: String, fifo: String): Actor = |
260 Simple_Thread.actor(name) { |
256 Simple_Thread.actor(name) { |
261 val stream = system.fifo_input_stream(out_fifo) // FIXME potentially blocking forever |
257 val stream = system.fifo_input_stream(fifo) // FIXME potentially blocking forever |
262 val default_buffer = new Array[Byte](65536) |
258 val default_buffer = new Array[Byte](65536) |
263 var c = -1 |
259 var c = -1 |
264 |
260 |
265 def read_chunk(): XML.Body = |
261 def read_chunk(): XML.Body = |
266 { |
262 { |
320 |
316 |
321 /** init **/ |
317 /** init **/ |
322 |
318 |
323 /* exec process */ |
319 /* exec process */ |
324 |
320 |
|
321 private val in_fifo = system.mk_fifo() |
|
322 private val out_fifo = system.mk_fifo() |
|
323 private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) } |
|
324 |
325 try { |
325 try { |
326 val cmdline = |
326 val cmdline = |
327 List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args |
327 List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args |
328 proc = Some(system.execute(true, cmdline: _*)) |
328 proc = Some(system.execute(true, cmdline: _*)) |
329 } |
329 } |
330 catch { |
330 catch { case e: IOException => rm_fifos(); throw(e) } |
331 case e: IOException => |
|
332 rm_fifos() |
|
333 error("Failed to execute Isabelle process: " + e.getMessage) |
|
334 } |
|
335 |
331 |
336 |
332 |
337 /* I/O actors */ |
333 /* I/O actors */ |
338 |
334 |
339 private val command_input = input_actor("command_input") |
335 private val command_input = input_actor("command_input", in_fifo) |
340 message_actor("message_output") |
336 message_actor("message_output", out_fifo) |
341 |
337 |
342 private val standard_input = stdin_actor("standard_input", proc.get.getOutputStream) |
338 private val standard_input = stdin_actor("standard_input", proc.get.getOutputStream) |
343 stdout_actor("standard_output", proc.get.getInputStream) |
339 stdout_actor("standard_output", proc.get.getInputStream) |
344 |
340 |
345 |
341 |
349 proc match { |
345 proc match { |
350 case None => |
346 case None => |
351 case Some(p) => |
347 case Some(p) => |
352 val rc = p.waitFor() |
348 val rc = p.waitFor() |
353 Thread.sleep(300) // FIXME property!? |
349 Thread.sleep(300) // FIXME property!? |
354 put_result(Markup.SYSTEM, "process_exit terminated") |
350 put_result(Markup.SYSTEM, "Isabelle process terminated") |
355 put_result(Markup.EXIT, rc.toString) |
351 put_result(Markup.EXIT, rc.toString) |
356 } |
352 } |
357 rm_fifos() |
353 rm_fifos() |
358 } |
354 } |
359 |
355 |