# HG changeset patch
# User wenzelm
# Date 1601380321 -7200
# Node ID 6916b48b375c3b8b8c959784d748dd06dc286466
# Parent  0823524eea1ec1c525e0c3945987a49c183d07a1
clarified names;

diff -r 0823524eea1e -r 6916b48b375c src/Pure/Concurrent/isabelle_thread.scala
--- a/src/Pure/Concurrent/isabelle_thread.scala	Tue Sep 29 13:20:27 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.scala	Tue Sep 29 13:52:01 2020 +0200
@@ -29,7 +29,11 @@
   private val counter = Counter.make()
 
   def make_name(name: String = "", base: String = "thread"): String =
-    "Isabelle." + proper_string(name).getOrElse(base + counter())
+  {
+    val prefix = "Isabelle."
+    val suffix = if (name.nonEmpty) name else base + counter()
+    if (suffix.startsWith(prefix)) suffix else prefix + suffix
+  }
 
   def current_thread_group: ThreadGroup = Thread.currentThread.getThreadGroup