src/Pure/ML-Systems/proper_int.ML
changeset 45067 d5156aa8556d
parent 45030 9cf265a192f6
child 50801 b8ff6d1ee56c
equal deleted inserted replaced
45066:11f622794ad6 45067:d5156aa8556d
    83       NONE => NONE
    83       NONE => NONE
    84     | SOME (c, d) => SOME (mk_int c, d));
    84     | SOME (c, d) => SOME (mk_int c, d));
    85 end;
    85 end;
    86 
    86 
    87 
    87 
       
    88 (* Word8VectorSlice *)
       
    89 
       
    90 structure Word8VectorSlice =
       
    91 struct
       
    92   open Word8VectorSlice;
       
    93   val length = mk_int o Word8VectorSlice.length;
       
    94   fun subslice (a, b, c) = Word8VectorSlice.subslice (a, dest_int b, Option.map dest_int c);
       
    95 end;
       
    96 
       
    97 
    88 (* Char *)
    98 (* Char *)
    89 
    99 
    90 structure Char =
   100 structure Char =
    91 struct
   101 struct
    92   open Char;
   102   open Char;
   245 end;
   255 end;
   246 
   256 
   247 
   257 
   248 (* Sockets *)
   258 (* Sockets *)
   249 
   259 
       
   260 structure Socket =
       
   261 struct
       
   262   open Socket;
       
   263   fun recvVec (a, b) = Socket.recvVec (a, dest_int b);
       
   264   fun sendVec a = mk_int (Socket.sendVec a);
       
   265 end;
       
   266 
   250 structure INetSock =
   267 structure INetSock =
   251 struct
   268 struct
   252   open INetSock;
   269   open INetSock;
   253   fun toAddr (a, b) = INetSock.toAddr (a, dest_int b);
   270   fun toAddr (a, b) = INetSock.toAddr (a, dest_int b);
   254   fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end;
   271   fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end;