lib/classes/isabelle/IsabelleProcess.java

             STDIN, STDOUT, STDERR, SIGNAL, EXIT,                        // Posix channels/events
             WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG, PROMPT,  // Isabelle messages
             SYSTEM                                                      // internal system notification
         };
         public Kind kind;
+        public Properties props;
         public String result;
 
-        public Result(Kind kind, String result) {
+        public Result(Kind kind, Properties props, String result) {
             this.kind = kind;
+            this.props = props;
             this.result = result;
         }
 
         public boolean isRaw() {
             return

               this.kind == Kind.PROMPT ||
               this.kind == Kind.SYSTEM;
         }
 
         public String toString() {
-            return this.kind.toString() + " [[" + this.result + "]]";
+            if (this.props == null) {
+                return this.kind.toString() + " [[" + this.result + "]]";
+            } else {
+                return this.kind.toString() + " " + props.toString() + " [[" + this.result + "]]";
+            }
         }
     }
 
 
     /**
      * Main result queue -- accumulates cooked messages asynchronously.
      */
     public LinkedBlockingQueue<Result> results;
 
+    private synchronized void putResult(Result.Kind kind, Properties props, String result) {
+        try {
+            results.put(new Result(kind, props, result));
+        } catch (InterruptedException exn) {  }
+    }
     private synchronized void putResult(Result.Kind kind, String result) {
-        try {
-            results.put(new Result(kind, result));
-        } catch (InterruptedException exn) {  }
+        putResult(kind, null, result);
     }
 
 
     /**
      * Interrupts Isabelle process via Posix signal.

     public synchronized void ML(Properties props, String text) throws IsabelleProcessException
     {
         command(props, "ML " + encodeString(text));
     }
 
-    
+
     /* input from the process (stdout/stderr) */
 
     private volatile BufferedReader inputReader;
     private class InputThread extends Thread
     {
         public void run()
         {
             Result.Kind kind = Result.Kind.STDOUT;
+            Properties props = null;
             StringBuffer buf = new StringBuffer(100);
 
             try {
                 while (inputReader != null) {
                     if (kind == Result.Kind.STDOUT && pid != null) {

                         }
                         if (buf.length() > 0) {
                             putResult(kind, buf.toString());
                             buf = new StringBuffer(100);
                         }
-                        if (c == 2) {
+                        if (c == -1) {
+                            inputReader.close();
+                            inputReader = null;
+                            tryClose();
+                        }
+                        else if (c == 2) {
                             c = inputReader.read();
                             switch (c) {
                                 case 'A': kind = Result.Kind.WRITELN; break;
                                 case 'B': kind = Result.Kind.PRIORITY; break;
                                 case 'C': kind = Result.Kind.TRACING; break;

                                 case 'E': kind = Result.Kind.ERROR; break;
                                 case 'F': kind = Result.Kind.DEBUG; break;
                                 case 'G': kind = Result.Kind.PROMPT; break;
                                 default: kind = Result.Kind.STDOUT; break;
                             }
-                        }
-                        if (c == -1) {
-                            inputReader.close();
-                            inputReader = null;
-                            tryClose();
+                            props = null;
                         }
                     } else {
                         // line mode
                         String line = null;
                         if ((line = inputReader.readLine()) != null) {

                                 buf.append("\n");
                                 putResult(kind, buf.toString());
                                 buf = new StringBuffer(100);
                             } else {
                                 int len = line.length();
-                                if (len >= 2 && line.charAt(len - 2) == 2 && line.charAt(len - 1) == '.') {
+                                // 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, buf.toString());
+                                    putResult(kind, props, buf.toString());
                                     buf = new StringBuffer(100);
                                     kind = Result.Kind.STDOUT;
-                                } else {
+                                }
+                                // text line
+                                else {
                                     buf.append(line);
                                     buf.append("\n");
                                 }
                             }
                         } else {