clarified workaround: problem is potential blocking of vacuous input (see also Poly/ML SVN 1874);
authorwenzelm
Wed, 16 Oct 2013 18:48:37 +0200
changeset 54345 fa80d47c6857
parent 54344 3ff2cb4bda76
child 54346 a3c59f04346f
clarified workaround: problem is potential blocking of vacuous input (see also Poly/ML SVN 1874);
src/Pure/System/system_channel.ML
--- a/src/Pure/System/system_channel.ML	Mon Oct 14 19:50:36 2013 +0200
+++ b/src/Pure/System/system_channel.ML	Wed Oct 16 18:48:37 2013 +0200
@@ -68,7 +68,9 @@
   in
     System_Channel
      {input_line = fn () => read_line in_stream,
-      inputN = fn n => if n = 0 then "" else Byte.bytesToString (BinIO.inputN (in_stream, n)),
+      inputN = fn n =>
+        if n = 0 then ""  (*workaround for polyml-5.5.1 or earlier*)
+        else Byte.bytesToString (BinIO.inputN (in_stream, n)),
       output = fn s => BinIO.output (out_stream, Byte.stringToBytes s),
       flush = fn () => BinIO.flushOut out_stream}
   end;