# HG changeset patch
# User wenzelm
# Date 1316782769 -7200
# Node ID 8b20be429cf33116fe4168cb36b3b5495c3ad9f9
# Parent  86c9b73158a89f9680b07eab504c0fbbb90a0a35
raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;

diff -r 86c9b73158a8 -r 8b20be429cf3 src/Pure/System/system_channel.ML
--- a/src/Pure/System/system_channel.ML	Fri Sep 23 14:13:15 2011 +0200
+++ b/src/Pure/System/system_channel.ML	Fri Sep 23 14:59:29 2011 +0200
@@ -47,31 +47,65 @@
   end;
 
 
-(* sockets *)
+(* sockets *)  (* FIXME raw unbuffered IO !?!? *)
+
+local
 
-fun read_line in_stream =
+fun readN socket n =
   let
-    fun result cs = String.implode (rev (#"\n" :: cs));
+    fun read i buf =
+      let
+        val s = Byte.bytesToString (Socket.recvVec (socket, n - i));
+        val m = size s;
+        val i' = i + m;
+        val buf' = Buffer.add s buf;
+      in if m > 0 andalso n > i' then read i' buf' else Buffer.content buf' end;
+  in read 0 Buffer.empty end;
+
+fun read_line socket =
+  let
+    fun result cs = implode (rev ("\n" :: cs));
     fun read cs =
-      (case BinIO.input1 in_stream of
-        NONE => if null cs then NONE else SOME (result cs)
-      | SOME b =>
-          (case Byte.byteToChar b of
-            #"\n" => SOME (result cs)
-          | c => read (c :: cs)));
+      (case readN socket 1 of
+        "" => if null cs then NONE else SOME (result cs)
+      | "\n" => SOME (result cs)
+      | c => read (c :: cs));
   in read [] end;
 
+fun write socket =
+  let
+    fun send buf =
+      if Word8VectorSlice.isEmpty buf then ()
+      else
+        let
+          val n = Int.min (Word8VectorSlice.length buf, 4096);
+          val m = Socket.sendVec (socket, Word8VectorSlice.subslice (buf, 0, SOME n));
+          val buf' = Word8VectorSlice.subslice (buf, m, NONE);
+        in send buf' end;
+  in fn s => send (Word8VectorSlice.full (Byte.stringToBytes s)) end;
+
+in
+
 fun socket_rendezvous name =
   let
-    val (in_stream, out_stream) = Socket_IO.open_streams name;
-    val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
+    fun err () = error ("Bad socket name: " ^ quote name);
+    val (host, port) =
+      (case space_explode ":" name of
+        [h, p] =>
+         (case NetHostDB.getByName h of SOME host => host | NONE => err (),
+          case Int.fromString p of SOME port => port | NONE => err ())
+      | _ => err ());
+    val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
+    val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
   in
     System_Channel
-     {input_line = fn () => read_line in_stream,
-      inputN = fn n => Byte.bytesToString (BinIO.inputN (in_stream, n)),
-      output = fn s => BinIO.output (out_stream, Byte.stringToBytes s),
-      flush = fn () => BinIO.flushOut out_stream}
+     {input_line = fn () => read_line socket,
+      inputN = fn n => readN socket n,
+      output = fn s => write socket s,
+      flush = fn () => ()}
   end;
 
 end;
 
+end;
+