# HG changeset patch
# User wenzelm
# Date 1708769111 -3600
# Node ID da4e82434985e5364185e87b415dbca96e2286d9
# Parent  f33d37c171a9f41013da0d3536b7bd255a473939
tuned signature;

diff -r f33d37c171a9 -r da4e82434985 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Sat Feb 24 10:55:16 2024 +0100
+++ b/src/Pure/Build/build.scala	Sat Feb 24 11:05:11 2024 +0100
@@ -39,7 +39,7 @@
     fresh_build: Boolean = false,
     no_build: Boolean = false,
     session_setup: (String, Session) => Unit = (_, _) => (),
-    build_uuid: String = UUID.random().toString,
+    build_uuid: String = UUID.random_string(),
     jobs: Int = 0,
     master: Boolean = false
   ) {
diff -r f33d37c171a9 -r da4e82434985 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Sat Feb 24 10:55:16 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Sat Feb 24 11:05:11 2024 +0100
@@ -898,7 +898,7 @@
     catch { case exn: Throwable => close(); throw exn }
 
   protected val (progress, worker_uuid) = synchronized {
-    if (_build_database.isEmpty) (build_progress, UUID.random().toString)
+    if (_build_database.isEmpty) (build_progress, UUID.random_string())
     else {
       try {
         val db = store.open_build_database(Progress.private_data.database, server = server)
diff -r f33d37c171a9 -r da4e82434985 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Sat Feb 24 10:55:16 2024 +0100
+++ b/src/Pure/General/http.scala	Sat Feb 24 11:05:11 2024 +0100
@@ -114,7 +114,7 @@
       connection.setRequestMethod("POST")
       connection.setDoOutput(true)
 
-      val boundary = UUID.random().toString
+      val boundary = UUID.random_string()
       connection.setRequestProperty(
         "Content-Type", "multipart/form-data; boundary=" + quote(boundary))
 
@@ -277,7 +277,7 @@
 
   def server(
     port: Int = 0,
-    name: String = UUID.random().toString,
+    name: String = UUID.random_string(),
     services: List[Service] = isabelle_services
   ): Server = {
     val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, port), 0)
diff -r f33d37c171a9 -r da4e82434985 src/Pure/General/uuid.scala
--- a/src/Pure/General/uuid.scala	Sat Feb 24 10:55:16 2024 +0100
+++ b/src/Pure/General/uuid.scala	Sat Feb 24 11:05:11 2024 +0100
@@ -11,6 +11,7 @@
   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 f33d37c171a9 -r da4e82434985 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sat Feb 24 10:55:16 2024 +0100
+++ b/src/Pure/System/progress.scala	Sat Feb 24 11:05:11 2024 +0100
@@ -274,7 +274,7 @@
   output_stopped: Boolean = false,
   kind: String = "progress",
   hostname: String = Isabelle_System.hostname(),
-  context_uuid: String = UUID.random().toString,
+  context_uuid: String = UUID.random_string(),
   timeout: Option[Time] = None)
 extends Progress {
   database_progress =>
@@ -299,7 +299,7 @@
       Progress.private_data.read_progress_context(db, context_uuid) match {
         case Some(context) =>
           _context = context
-          _agent_uuid = UUID.random().toString
+          _agent_uuid = UUID.random_string()
         case None =>
           _context = Progress.private_data.next_progress_context(db)
           _agent_uuid = context_uuid
diff -r f33d37c171a9 -r da4e82434985 src/Pure/System/system_channel.scala
--- a/src/Pure/System/system_channel.scala	Sat Feb 24 10:55:16 2024 +0100
+++ b/src/Pure/System/system_channel.scala	Sat Feb 24 11:05:11 2024 +0100
@@ -46,7 +46,7 @@
   protected val server: ServerSocketChannel = ServerSocketChannel.open(protocol_family)
 
   def address: String
-  lazy val password: String = UUID.random().toString
+  lazy val password: String = UUID.random_string()
 
   override def toString: String = address
 
diff -r f33d37c171a9 -r da4e82434985 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Feb 24 10:55:16 2024 +0100
+++ b/src/Pure/Tools/server.scala	Sat Feb 24 11:05:11 2024 +0100
@@ -121,7 +121,7 @@
     val socket: ServerSocket = new ServerSocket(port0, 50, Server.localhost)
     def port: Int = socket.getLocalPort
     def address: String = print_address(port)
-    val password: String = UUID.random().toString
+    val password: String = UUID.random_string()
 
     override def toString: String = print(port, password)
 
diff -r f33d37c171a9 -r da4e82434985 src/Tools/VSCode/src/component_vscode_extension.scala
--- a/src/Tools/VSCode/src/component_vscode_extension.scala	Sat Feb 24 10:55:16 2024 +0100
+++ b/src/Tools/VSCode/src/component_vscode_extension.scala	Sat Feb 24 11:05:11 2024 +0100
@@ -48,7 +48,7 @@
   "name": "Isabelle",
   "scopeName": "source.isabelle",
   "fileTypes": ["thy"],
-  "uuid": """ + JSON.Format(UUID.random().toString) + """,
+  "uuid": """ + JSON.Format(UUID.random_string()) + """,
   "repository": {
     "comment": {
       "patterns": [
diff -r f33d37c171a9 -r da4e82434985 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Sat Feb 24 10:55:16 2024 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Sat Feb 24 11:05:11 2024 +0100
@@ -390,7 +390,7 @@
 
   /* HTTP server */
 
-  val http_root: String = "/" + UUID.random().toString
+  val http_root: String = "/" + UUID.random_string()
 
   val http_server: HTTP.Server =
     HTTP.server(services = Document_Model.Preview_Service :: HTTP.isabelle_services)