--- 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