more robust: avoid duplicate Socket.close;
authorwenzelm
Sun Feb 10 22:24:22 2019 +0100 (2 months ago)
changeset 6979918cb541a975f
parent 69798 f610115ca3d0
child 69800 74c1a0643010
more robust: avoid duplicate Socket.close;
src/Pure/General/socket_io.ML
     1.1 --- a/src/Pure/General/socket_io.ML	Sun Feb 10 19:07:53 2019 +0100
     1.2 +++ b/src/Pure/General/socket_io.ML	Sun Feb 10 22:24:22 2019 +0100
     1.3 @@ -16,6 +16,9 @@
     1.4  structure Socket_IO: SOCKET_IO =
     1.5  struct
     1.6  
     1.7 +fun close_permissive socket =
     1.8 +  Socket.close socket handle OS.SysErr _ => ();
     1.9 +
    1.10  fun make_streams socket =
    1.11    let
    1.12      val (host, port) = INetSock.fromAddr (Socket.Ctl.getSockName socket);
    1.13 @@ -36,7 +39,7 @@
    1.14          setPos = NONE,
    1.15          endPos = NONE,
    1.16          verifyPos = NONE,
    1.17 -        close = fn () => Socket.close socket,
    1.18 +        close = fn () => close_permissive socket,
    1.19          ioDesc = NONE
    1.20        };
    1.21  
    1.22 @@ -54,7 +57,7 @@
    1.23          setPos = NONE,
    1.24          endPos = NONE,
    1.25          verifyPos = NONE,
    1.26 -        close = fn () => Socket.close socket,
    1.27 +        close = fn () => close_permissive socket,
    1.28          ioDesc = NONE
    1.29        };
    1.30