--- a/src/Pure/ML-Systems/proper_int.ML Fri Sep 23 17:23:54 2011 +0200
+++ b/src/Pure/ML-Systems/proper_int.ML Fri Sep 23 17:35:06 2011 +0200
@@ -85,6 +85,16 @@
end;
+(* Word8VectorSlice *)
+
+structure Word8VectorSlice =
+struct
+ open Word8VectorSlice;
+ val length = mk_int o Word8VectorSlice.length;
+ fun subslice (a, b, c) = Word8VectorSlice.subslice (a, dest_int b, Option.map dest_int c);
+end;
+
+
(* Char *)
structure Char =
@@ -247,6 +257,13 @@
(* Sockets *)
+structure Socket =
+struct
+ open Socket;
+ fun recvVec (a, b) = Socket.recvVec (a, dest_int b);
+ fun sendVec a = mk_int (Socket.sendVec a);
+end;
+
structure INetSock =
struct
open INetSock;