more robust open/close bracket, but with potential danger of blocking indefinitely in uninterruptible state;

--- a/src/Pure/General/file.ML	Wed Dec 19 21:37:48 2018 +0100
+++ b/src/Pure/General/file.ML	Wed Dec 19 21:38:57 2018 +0100
@@ -92,9 +92,12 @@
 
 local
 
-fun with_file open_file close_file f path =
-  let val file = open_file path
-  in Exn.release (Exn.capture f file before close_file file) end;
+fun with_file open_file close_file f =
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn path =>
+    let
+      val file = open_file path;
+      val result = Exn.capture (restore_attributes f) file;
+    in close_file file; Exn.release result end);
 
 in
 

--- a/src/Pure/General/socket_io.ML	Wed Dec 19 21:37:48 2018 +0100
+++ b/src/Pure/General/socket_io.ML	Wed Dec 19 21:38:57 2018 +0100
@@ -10,6 +10,7 @@
 sig
   val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
   val open_streams: string -> BinIO.instream * BinIO.outstream
+  val with_streams: (BinIO.instream * BinIO.outstream -> 'a) -> string -> 'a
 end;
 
 structure Socket_IO: SOCKET_IO =
@@ -81,5 +82,11 @@
     val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
   in make_streams socket end;
 
+fun with_streams f =
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn socket_name =>
+    let
+      val streams = open_streams socket_name;
+      val result = Exn.capture (restore_attributes f) streams;
+    in BinIO.closeIn (#1 streams); BinIO.closeOut (#2 streams); Exn.release result end);
+
 end;
-