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