# HG changeset patch
# User wenzelm
# Date 1628766790 -7200
# Node ID 8d20b1cf0d5da3e154e3abe290aae2993c2c850f
# Parent  0f051404f487cf5e826548f4f5d35ddcf40c325e
clarified signature;
clarified errors;

diff -r 0f051404f487 -r 8d20b1cf0d5d src/Pure/General/socket_io.ML
--- a/src/Pure/General/socket_io.ML	Sat Aug 07 22:23:37 2021 +0200
+++ b/src/Pure/General/socket_io.ML	Thu Aug 12 13:13:10 2021 +0200
@@ -11,6 +11,7 @@
   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
+  val with_streams': (BinIO.instream * BinIO.outstream -> 'a) -> string -> string -> 'a
 end;
 
 structure Socket_IO: SOCKET_IO =
@@ -83,7 +84,8 @@
       | _ => err ());
     val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
     val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
-  in make_streams socket end;
+  in make_streams socket end
+  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 =>
@@ -92,4 +94,8 @@
       val result = Exn.capture (restore_attributes f) streams;
     in BinIO.closeIn (#1 streams); BinIO.closeOut (#2 streams); Exn.release result end);
 
+fun with_streams' f socket_name password =
+  with_streams (fn streams =>
+    (Byte_Message.write_line (#2 streams) password; f streams)) socket_name;
+
 end;
diff -r 0f051404f487 -r 8d20b1cf0d5d src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Aug 07 22:23:37 2021 +0200
+++ b/src/Pure/ROOT.ML	Thu Aug 12 13:13:10 2021 +0200
@@ -81,7 +81,6 @@
 ML_file "General/file.ML";
 ML_file "General/long_name.ML";
 ML_file "General/binding.ML";
-ML_file "General/socket_io.ML";
 ML_file "General/seq.ML";
 ML_file "General/time.ML";
 ML_file "General/timing.ML";
@@ -92,6 +91,7 @@
 ML_file "PIDE/byte_message.ML";
 ML_file "PIDE/protocol_message.ML";
 ML_file "PIDE/document_id.ML";
+ML_file "General/socket_io.ML";
 
 ML_file "General/change_table.ML";
 ML_file "General/graph.ML";