# HG changeset patch
# User wenzelm
# Date 1627739051 -7200
# Node ID 6113f1db43429291e844e8606d532862aa938e8b
# Parent  dc962d4248ca65924e2c2a84d4f63d8a8a3295bb
clarified signature;

diff -r dc962d4248ca -r 6113f1db4342 src/Pure/General/http.scala
--- 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))
 
diff -r dc962d4248ca -r 6113f1db4342 src/Pure/General/uuid.scala
--- 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)) }
diff -r dc962d4248ca -r 6113f1db4342 src/Pure/Tools/server.scala
--- 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)
 
diff -r dc962d4248ca -r 6113f1db4342 src/Tools/VSCode/src/textmate_grammar.scala
--- 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": [
diff -r dc962d4248ca -r 6113f1db4342 src/Tools/jEdit/src/main_plugin.scala
--- 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))