# 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
   }