# HG changeset patch
# User wenzelm
# Date 1281382545 -7200
# Node ID bf44a85c74ccc7262343edbef9b224072ad033d4
# Parent  fb1b255d6e36a07d1be98059d08fcd001e7e99b9
uniform raw_dump for input/output fifos on Cygwin;

diff -r fb1b255d6e36 -r bf44a85c74cc lib/scripts/raw_dump
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/raw_dump	Mon Aug 09 21:35:45 2010 +0200
@@ -0,0 +1,56 @@
+#!/usr/bin/env perl
+#
+# Author: Makarius
+#
+# raw_dump - direct copy without extra buffering
+#
+
+use warnings;
+use strict;
+
+use IO::File;
+
+
+# args
+
+my ($input, $output) = @ARGV;
+
+
+# prepare files
+
+my $infile;
+my $outfile;
+
+if ($input eq "-") { $infile = *STDIN; }
+else {
+  $infile = new IO::File $input, "r";
+  defined $infile || die $!;
+}
+
+if ($output eq "-") { $outfile = *STDOUT; }
+else {
+  $outfile = new IO::File $output, "w";
+  defined $outfile || die $!;
+}
+
+binmode $infile;
+binmode $outfile;
+
+
+# main loop
+
+my $chunk;
+while ((sysread $infile, $chunk, 65536), length $chunk > 0) {
+  my $end = length $chunk;
+  my $offset = 0;
+  while ($offset < $end) {
+    $offset += syswrite $outfile, $chunk, $end - $offset, $offset;
+  }
+}
+
+
+# cleanup
+
+undef $infile;
+undef $outfile;
+
diff -r fb1b255d6e36 -r bf44a85c74cc src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Aug 09 21:23:24 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Aug 09 21:35:45 2010 +0200
@@ -291,9 +291,8 @@
   {
     // block until peer is ready
     val stream =
-      if (Platform.is_windows) {
-        // Cygwin fifo as Windows/Java input stream
-        val proc = execute(false, "cat", fifo)
+      if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
+        val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), fifo, "-")
         proc.getOutputStream.close
         proc.getErrorStream.close
         proc.getInputStream
@@ -306,14 +305,8 @@
   {
     // 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)
+      if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
+        val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), "-", fifo)
         proc.getInputStream.close
         proc.getErrorStream.close
         val out = proc.getOutputStream
@@ -324,7 +317,6 @@
           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)