--- a/src/Pure/General/socket_io.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/General/socket_io.ML Tue Sep 26 12:46:31 2023 +0200
@@ -88,10 +88,10 @@
handle OS.SysErr (msg, _) => error (msg ^ ": failed to open socket " ^ socket_name);
fun with_streams f =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn socket_name =>
+ Thread_Attributes.uninterruptible (fn run => fn socket_name =>
let
val streams = open_streams socket_name;
- val result = Exn.capture (restore_attributes f) streams;
+ val result = Exn.capture (run f) streams;
in BinIO.closeIn (#1 streams); BinIO.closeOut (#2 streams); Exn.release result end);
fun with_streams' f socket_name password =