src/Pure/General/socket_io.ML

--- a/src/Pure/General/socket_io.ML	Sun Feb 10 19:07:53 2019 +0100
+++ b/src/Pure/General/socket_io.ML	Sun Feb 10 22:24:22 2019 +0100
@@ -16,6 +16,9 @@
 structure Socket_IO: SOCKET_IO =
 struct
 
+fun close_permissive socket =
+  Socket.close socket handle OS.SysErr _ => ();
+
 fun make_streams socket =
   let
     val (host, port) = INetSock.fromAddr (Socket.Ctl.getSockName socket);
@@ -36,7 +39,7 @@
         setPos = NONE,
         endPos = NONE,
         verifyPos = NONE,
-        close = fn () => Socket.close socket,
+        close = fn () => close_permissive socket,
         ioDesc = NONE
       };
 
@@ -54,7 +57,7 @@
         setPos = NONE,
         endPos = NONE,
         verifyPos = NONE,
-        close = fn () => Socket.close socket,
+        close = fn () => close_permissive socket,
         ioDesc = NONE
       };