# HG changeset patch
# User wenzelm
# Date 1610808234 -3600
# Node ID 497e11537d48fc22775c5f8f5c7979092728bc26
# Parent  479668d61cef847dfc8d4e26cc2217828a27e3e9
clarified signature: more operations;

diff -r 479668d61cef -r 497e11537d48 src/Pure/General/uuid.scala
--- a/src/Pure/General/uuid.scala	Fri Jan 15 14:11:01 2021 +0100
+++ b/src/Pure/General/uuid.scala	Sat Jan 16 15:43:54 2021 +0100
@@ -17,4 +17,6 @@
   def unapply(s: String): Option[T] =
     try { Some(java.util.UUID.fromString(s)) }
     catch { case _: IllegalArgumentException => None }
+
+  def unapply(body: XML.Body): Option[T] = unapply(XML.content(body))
 }
diff -r 479668d61cef -r 497e11537d48 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Jan 15 14:11:01 2021 +0100
+++ b/src/Pure/Tools/server.scala	Sat Jan 16 15:43:54 2021 +0100
@@ -150,6 +150,7 @@
 
     def start { thread }
     def join { thread.join }
+    def stop { socket.close; join }
   }
 
 
@@ -187,6 +188,10 @@
       try { Byte_Message.read_line_message(in).map(_.text) }
       catch { case _: IOException => None }
 
+    def await_close(): Unit =
+      try { Byte_Message.read(in, 1) }
+      catch { case _: IOException => }
+
     def write_message(msg: String): Unit =
       out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) }