# HG changeset patch # User wenzelm # Date 1199565438 -3600 # Node ID 2a7efcfe9b5416ca83127055572bf78b7c907401 # Parent f7771e4f7064bd14c115c2d5fa3bc93bf2539efe added INIT message, with pid and session property; removed adhoc PID handling; diff -r f7771e4f7064 -r 2a7efcfe9b54 lib/classes/isabelle/IsabelleProcess.java --- a/lib/classes/isabelle/IsabelleProcess.java Sat Jan 05 09:16:27 2008 +0100 +++ b/lib/classes/isabelle/IsabelleProcess.java Sat Jan 05 21:37:18 2008 +0100 @@ -29,6 +29,7 @@ * * @@ -52,7 +53,9 @@ private volatile boolean closing = false; private LinkedBlockingQueue output = null; + public volatile String session = null; + /** * Models failures in process management. */ @@ -71,9 +74,9 @@ */ public static class Result { public enum Kind { - STDIN, STDOUT, STDERR, SIGNAL, EXIT, // Posix channels/events - WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG, PROMPT, // Isabelle messages - SYSTEM // internal system notification + STDIN, STDOUT, STDERR, SIGNAL, EXIT, // Posix channels/events + WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG, PROMPT, INIT, // Isabelle messages + SYSTEM // internal system notification }; public Kind kind; public Properties props; @@ -100,6 +103,7 @@ this.kind == Kind.SYSTEM; } + @Override public String toString() { if (this.props == null) { return this.kind.toString() + " [[" + this.result + "]]"; @@ -344,7 +348,7 @@ try { while (inputReader != null) { - if (kind == Result.Kind.STDOUT && pid != null) { + if (kind == Result.Kind.STDOUT) { // char mode int c = -1; while ((buf.length() == 0 || inputReader.ready()) && @@ -370,6 +374,7 @@ case 'E': kind = Result.Kind.ERROR; break; case 'F': kind = Result.Kind.DEBUG; break; case 'G': kind = Result.Kind.PROMPT; break; + case 'H': kind = Result.Kind.INIT; break; default: kind = Result.Kind.STDOUT; break; } props = null; @@ -378,40 +383,35 @@ // line mode String line = null; if ((line = inputReader.readLine()) != null) { - if (pid == null && kind == Result.Kind.STDOUT && line.startsWith("PID=")) { - pid = line.substring("PID=".length()); - } else if (kind == Result.Kind.STDOUT) { + int len = line.length(); + // property + if (line.endsWith("\u0002,")) { + int i = line.indexOf("="); + if (i > 0) { + String name = line.substring(0, i); + String 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.")) { + if (kind == Result.Kind.INIT && props != null) { + pid = props.getProperty("pid"); + session = props.getProperty("session"); + } + buf.append(line.substring(0, len - 2)); + putResult(kind, props, buf.toString()); + buf = new StringBuffer(100); + kind = Result.Kind.STDOUT; + } + // text line + else { buf.append(line); buf.append("\n"); - putResult(kind, buf.toString()); - buf = new StringBuffer(100); - } else { - int len = line.length(); - // property - if (line.endsWith("\u0002,")) { - int i = line.indexOf("="); - if (i > 0) { - String name = line.substring(0, i); - String 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.")) { - buf.append(line.substring(0, len - 2)); - putResult(kind, props, buf.toString()); - buf = new StringBuffer(100); - kind = Result.Kind.STDOUT; - } - // text line - else { - buf.append(line); - buf.append("\n"); - } } } else { inputReader.close();