clarified signature;

--- a/src/Pure/General/http.scala	Sat Jul 31 12:48:01 2021 +0200
+++ b/src/Pure/General/http.scala	Sat Jul 31 15:44:11 2021 +0200
@@ -105,7 +105,7 @@
       connection.setRequestMethod("POST")
       connection.setDoOutput(true)
 
-      val boundary = UUID.random_string()
+      val boundary = UUID.random().toString
       connection.setRequestProperty(
         "Content-Type", "multipart/form-data; boundary=" + quote(boundary))
 

--- a/src/Pure/General/uuid.scala	Sat Jul 31 12:48:01 2021 +0200
+++ b/src/Pure/General/uuid.scala	Sat Jul 31 15:44:11 2021 +0200
@@ -12,7 +12,6 @@
   type T = java.util.UUID
 
   def random(): T = java.util.UUID.randomUUID()
-  def random_string(): String = random().toString
 
   def unapply(s: String): Option[T] =
     try { Some(java.util.UUID.fromString(s)) }

--- a/src/Pure/Tools/server.scala	Sat Jul 31 12:48:01 2021 +0200
+++ b/src/Pure/Tools/server.scala	Sat Jul 31 15:44:11 2021 +0200
@@ -128,7 +128,7 @@
   {
     val socket: ServerSocket = new ServerSocket(port0, 50, Server.localhost)
     def port: Int = socket.getLocalPort
-    val password: String = UUID.random_string()
+    val password: String = UUID.random().toString
 
     override def toString: String = print(port, password)
 

--- a/src/Tools/VSCode/src/textmate_grammar.scala	Sat Jul 31 12:48:01 2021 +0200
+++ b/src/Tools/VSCode/src/textmate_grammar.scala	Sat Jul 31 15:44:11 2021 +0200
@@ -45,7 +45,7 @@
   "name": "Isabelle",
   "scopeName": "source.isabelle",
   "fileTypes": ["thy"],
-  "uuid": """ + JSON.Format(UUID.random_string()) + """,
+  "uuid": """ + JSON.Format(UUID.random().toString) + """,
   "repository": {
     "comment": {
       "patterns": [

--- a/src/Tools/jEdit/src/main_plugin.scala	Sat Jul 31 12:48:01 2021 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Sat Jul 31 15:44:11 2021 +0200
@@ -427,7 +427,7 @@
 
   /* HTTP server */
 
-  val http_root: String = "/" + UUID.random()
+  val http_root: String = "/" + UUID.random().toString
 
   val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))