src/Pure/System/isabelle_system.scala

--- a/src/Pure/System/isabelle_system.scala	Mon Aug 09 13:56:02 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Aug 09 18:18:32 2010 +0200
@@ -8,9 +8,8 @@
 
 import java.util.regex.Pattern
 import java.util.Locale
-import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
-  BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
-  File, IOException}
+import java.io.{BufferedInputStream, FileInputStream, BufferedOutputStream, FileOutputStream,
+  OutputStream, File, IOException}
 import java.awt.{GraphicsEnvironment, Font}
 import java.awt.font.TextAttribute
 
@@ -288,11 +287,12 @@
     if (rc != 0) error(result)
   }
 
-  def fifo_stream(fifo: String): BufferedInputStream =
+  def fifo_input_stream(fifo: String): BufferedInputStream =
   {
-    // blocks until writer is ready
+    // block until peer is ready
     val stream =
       if (Platform.is_windows) {
+        // Cygwin fifo as Windows/Java input stream
         val proc = execute(false, "cat", fifo)
         proc.getOutputStream.close
         proc.getErrorStream.close
@@ -302,6 +302,34 @@
     new BufferedInputStream(stream)
   }
 
+  def fifo_output_stream(fifo: String): BufferedOutputStream =
+  {
+    // block until peer is ready
+    val stream =
+      if (Platform.is_windows) {
+        // Cygwin fifo as Windows/Java output stream (beware of buffering)
+        // FIXME FIXME FIXME
+        val script =
+          "open(FIFO, \">" + fifo + "\") || die $!; my $buffer; " +
+          "while ((sysread STDIN, $buffer, 65536), length $buffer > 0)" +
+          " { syswrite FIFO, $buffer; }; close FIFO;"
+        val proc = execute(false, "perl", "-e", script)
+        proc.getInputStream.close
+        proc.getErrorStream.close
+        val out = proc.getOutputStream
+        new OutputStream {
+          override def close() { out.close(); proc.waitFor() }
+          override def flush() { out.flush() }
+          override def write(b: Array[Byte]) { out.write(b) }
+          override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
+          override def write(b: Int) { out.write(b) }
+        }
+        proc.getOutputStream
+      }
+      else new FileOutputStream(fifo)
+    new BufferedOutputStream(stream)
+  }
+
 
 
   /** Isabelle resources **/