src/Pure/System/system_channel.ML

--- a/src/Pure/System/system_channel.ML	Wed Jan 09 22:38:21 2013 +0100
+++ b/src/Pure/System/system_channel.ML	Thu Jan 10 12:41:53 2013 +0100
@@ -47,65 +47,31 @@
   end;
 
 
-(* sockets *)  (* FIXME proper buffering via BinIO (after Poly/ML 5.4.1) *)
+(* sockets *)
 
-local
-
-fun readN socket n =
+fun read_line in_stream =
   let
-    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 result cs = String.implode (rev (#"\n" :: cs));
     fun read cs =
-      (case readN socket 1 of
-        "" => if null cs then NONE else SOME (result cs)
-      | "\n" => SOME (result cs)
-      | c => read (c :: 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)));
   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
-    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));
+    val (in_stream, out_stream) = Socket_IO.open_streams name;
+    val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
   in
     System_Channel
-     {input_line = fn () => read_line socket,
-      inputN = fn n => readN socket n,
-      output = fn s => write socket s,
-      flush = fn () => ()}
+     {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}
   end;
 
 end;
 
-end;
-