# HG changeset patch
# User wenzelm
# Date 1586085569 -7200
# Node ID f249b5c0fea221b363834f9e7d63b8ebdea09ab2
# Parent  f8e52c0152fe37e1021c6900d1b53011ba8651f1
clarified names;

diff -r f8e52c0152fe -r f249b5c0fea2 src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Sun Apr 05 13:05:40 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Sun Apr 05 13:19:29 2020 +0200
@@ -39,7 +39,7 @@
   | SOME name => name);
 
 fun set_name base =
-  Thread_Data.put name_var (SOME (base ^ "/" ^ string_of_int (count ())));
+  Thread_Data.put name_var (SOME ("Isabelle." ^ base ^ "-" ^ string_of_int (count ())));
 
 end;
 
diff -r f8e52c0152fe -r f249b5c0fea2 src/Pure/Concurrent/isabelle_thread.scala
--- a/src/Pure/Concurrent/isabelle_thread.scala	Sun Apr 05 13:05:40 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.scala	Sun Apr 05 13:19:29 2020 +0200
@@ -17,7 +17,7 @@
   private val counter = Counter.make()
 
   def make_name(name: String = "", base: String = "thread"): String =
-    proper_string(name).getOrElse(base + counter())
+    "Isabelle." + proper_string(name).getOrElse(base + counter())
 
   def current_thread_group: ThreadGroup = Thread.currentThread.getThreadGroup