# HG changeset patch
# User wenzelm
# Date 1549833862 -3600
# Node ID 18cb541a975f6f4ef60f8586d8c569cc0b34e01a
# Parent  f610115ca3d0e7d299627e0577ea11b37e1ffc91
more robust: avoid duplicate Socket.close;

diff -r f610115ca3d0 -r 18cb541a975f 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
       };