# HG changeset patch # User wenzelm # Date 1219944598 -7200 # Node ID 1a6f273108aed314735e7150867d12b2298c48fc # Parent e4b569b53e104c6832a574637ccd74195373db0e join stdout/stderr, eliminated Kind.STDERR; messages are read from separate fifo (ensures that spurious stdout from shell wrappers, Poly/ML runtime system etc. do not spoil message protocol); private output, output_raw; diff -r e4b569b53e10 -r 1a6f273108ae src/Pure/Tools/isabelle_process.scala --- a/src/Pure/Tools/isabelle_process.scala Thu Aug 28 19:29:57 2008 +0200 +++ b/src/Pure/Tools/isabelle_process.scala Thu Aug 28 19:29:58 2008 +0200 @@ -10,13 +10,17 @@ import java.util.Properties import java.util.concurrent.LinkedBlockingQueue -import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, IOException} +import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, + InputStream, OutputStream, FileInputStream, IOException} import isabelle.{Symbol, XML} object IsabelleProcess { + private val charset = "UTF-8" + + /* results */ object Kind extends Enumeration { @@ -24,7 +28,6 @@ // Posix channels/events val STDIN = Value("STDIN") val STDOUT = Value("STDOUT") - val STDERR = Value("STDERR") val SIGNAL = Value("SIGNAL") val EXIT = Value("EXIT") // Isabelle messages @@ -41,8 +44,7 @@ val SYSTEM = Value("SYSTEM") //}}} def is_raw(kind: Value) = - kind == STDOUT || - kind == STDERR + kind == STDOUT def is_control(kind: Value) = kind == SIGNAL || kind == EXIT || @@ -137,13 +139,14 @@ private val output = new LinkedBlockingQueue[String] - def output_raw(text: String) = synchronized { + private def output_raw(text: String) = synchronized { if (proc == null) error("Cannot output to Isabelle: no process") if (closing) error("Cannot output to Isabelle: already closing") output.put(text) } - def output_sync(text: String) = output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n") + private def output_sync(text: String) = + output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n") def command(text: String) = @@ -171,8 +174,9 @@ /* stdin */ - private class StdinThread(writer: BufferedWriter) extends Thread { + private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") { override def run() = { + val writer = new BufferedWriter(new OutputStreamWriter(out_stream, charset)) var finished = false while (!finished) { try { @@ -200,85 +204,32 @@ /* stdout */ - private class StdoutThread(reader: BufferedReader) extends Thread { + private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") { override def run() = { - var kind = Kind.STDOUT - var props: Properties = null - var result = new StringBuilder + val reader = new BufferedReader(new InputStreamReader(in_stream, charset)) + var result = new StringBuilder(100) var finished = false while (!finished) { try { - if (kind == Kind.STDOUT) { - //{{{ Char mode - var c = -1 - var done = false - while (!done && (result.length == 0 || reader.ready)) { - c = reader.read - if (c > 0 && c != 2) result.append(c.asInstanceOf[Char]) - else done = true - } - if (result.length > 0) { - put_result(kind, null, result.toString) - result.length = 0 - } - if (c == -1) { - reader.close - finished = true - try_close() - } - else if (c == 2) { - reader.read match { - case 'A' => kind = Kind.WRITELN - case 'B' => kind = Kind.PRIORITY - case 'C' => kind = Kind.TRACING - case 'D' => kind = Kind.WARNING - case 'E' => kind = Kind.ERROR - case 'F' => kind = Kind.DEBUG - case 'G' => kind = Kind.PROMPT - case 'H' => kind = Kind.INIT - case 'I' => kind = Kind.STATUS - case _ => kind = Kind.STDOUT - } - props = null - } - //}}} + //{{{ + var c = -1 + var done = false + while (!done && (result.length == 0 || reader.ready)) { + c = reader.read + if (c >= 0) result.append(c.asInstanceOf[Char]) + else done = true + } + if (result.length > 0) { + put_result(Kind.STDOUT, null, result.toString) + result.length = 0 } else { - //{{{ Line mode - val line = reader.readLine - if (line == null) { - reader.close - finished = true - try_close() - } - else { - val len = line.length - // property - if (line.endsWith("\u0002,")) { - val i = line.indexOf('=') - if (i > 0) { - val name = line.substring(0, i) - val value = line.substring(i + 1, len - 2) - if (props == null) props = new Properties - if (!props.containsKey(name)) props.setProperty(name, value) - } - } - // last text line - else if (line.endsWith("\u0002.")) { - result.append(line.substring(0, len - 2)) - put_result(kind, props, result.toString) - result.length = 0 - kind = Kind.STDOUT - } - // text line - else { - result.append(line) - result.append('\n') - } - } - //}}} + reader.close + finished = true + try_close() } + //}}} } catch { case e: IOException => put_result(Kind.SYSTEM, null, "Stdout thread: " + e.getMessage) @@ -289,76 +240,150 @@ } - /* stderr */ + /* messages */ - private class StderrThread(reader: BufferedReader) extends Thread { + private class MessageThread(fifo: String) extends Thread("isabelle: messages") { override def run() = { - var result = new StringBuilder(100) + val reader = new BufferedReader(new InputStreamReader(new FileInputStream(fifo), charset)) + var kind: Kind.Value = null + var props: Properties = null + var result = new StringBuilder var finished = false while (!finished) { try { - //{{{ - var c = -1 - var done = false - while (!done && (result.length == 0 || reader.ready)) { - c = reader.read - if (c > 0) result.append(c.asInstanceOf[Char]) - else done = true - } - if (result.length > 0) { - put_result(Kind.STDERR, null, result.toString) - result.length = 0 + try { + if (kind == null) { + //{{{ Char mode -- resync + var c = -1 + do { + c = reader.read + if (c >= 0 && c != 2) result.append(c.asInstanceOf[Char]) + } while (c >= 0 && c != 2) + + if (result.length > 0) { + put_result(Kind.SYSTEM, null, "Malformed message:\n" + result.toString) + result.length = 0 + } + if (c < 0) { + reader.close + finished = true + try_close() + } + else { + reader.read match { + case 'A' => kind = Kind.WRITELN + case 'B' => kind = Kind.PRIORITY + case 'C' => kind = Kind.TRACING + case 'D' => kind = Kind.WARNING + case 'E' => kind = Kind.ERROR + case 'F' => kind = Kind.DEBUG + case 'G' => kind = Kind.PROMPT + case 'H' => kind = Kind.INIT + case 'I' => kind = Kind.STATUS + case _ => kind = null + } + props = null + } + //}}} + } + else { + //{{{ Line mode + val line = reader.readLine + if (line == null) { + reader.close + finished = true + try_close() + } + else { + val len = line.length + // property + if (line.endsWith("\u0002,")) { + val i = line.indexOf('=') + if (i > 0) { + val name = line.substring(0, i) + val value = line.substring(i + 1, len - 2) + if (props == null) props = new Properties + if (!props.containsKey(name)) props.setProperty(name, value) + } + } + // last text line + else if (line.endsWith("\u0002.")) { + result.append(line.substring(0, len - 2)) + put_result(kind, props, result.toString) + result.length = 0 + kind = null + } + // text line + else { + result.append(line) + result.append('\n') + } + } + //}}} + } } - else { - reader.close - finished = true - try_close() + catch { + case e: IOException => put_result(Kind.SYSTEM, null, "Message thread: " + e.getMessage) } - //}}} } - catch { - case e: IOException => put_result(Kind.SYSTEM, null, "Stderr thread: " + e.getMessage) - } + catch { case _: InterruptedException => finished = true } } - put_result(Kind.SYSTEM, null, "Stderr thread terminated") + try { put_result(Kind.SYSTEM, null, "Message thread terminated") } + catch { case _ : InterruptedException => } } } - /* exit */ - - private class ExitThread extends Thread { - override def run() = { - val rc = proc.waitFor() - Thread.sleep(300) - put_result(Kind.SYSTEM, null, "Exit thread terminated") - put_result(Kind.EXIT, null, Integer.toString(rc)) - } - } - - - /** main **/ { + + /* message fifo */ + + val fifo = + try { + val mkfifo = IsabelleSystem.exec(List(IsabelleSystem.getenv_strict("ISATOOL"), "mkfifo")) + val fifo = new BufferedReader(new InputStreamReader(mkfifo.getInputStream, charset)).readLine + if (mkfifo.waitFor == 0) fifo + else error("Failed to create message fifo") + } + catch { + case e: IOException => error("Failed to create message fifo: " + e.getMessage) + } + + val message_thread = new MessageThread(fifo) + + /* exec process */ try { - proc = IsabelleSystem.exec(List( - IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W") ++ args) + proc = IsabelleSystem.exec2(List( + IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W", fifo) ++ args) } catch { case e: IOException => error("Failed to execute Isabelle process: " + e.getMessage) } - /* control process via threads */ + /* stdin/stdout */ + + new StdinThread(proc.getOutputStream).start + new StdoutThread(proc.getInputStream).start + + + /* exit */ - val charset = "UTF-8" - new StdinThread(new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, charset))).start - new StdoutThread(new BufferedReader(new InputStreamReader(proc.getInputStream, charset))).start - new StderrThread(new BufferedReader(new InputStreamReader(proc.getErrorStream, charset))).start + class ExitThread extends Thread("isabelle: exit") { + override def run() = { + val rc = proc.waitFor() + Thread.sleep(300) + put_result(Kind.SYSTEM, null, "Exit thread terminated") + put_result(Kind.EXIT, null, Integer.toString(rc)) + message_thread.interrupt + } + } + message_thread.start new ExitThread().start }