clarified names;
authorwenzelm
Sun, 05 Apr 2020 13:19:29 +0200
changeset 71693 f249b5c0fea2
parent 71692 f8e52c0152fe
child 71694 16aa085f9353
clarified names;
src/Pure/Concurrent/isabelle_thread.ML
src/Pure/Concurrent/isabelle_thread.scala
--- 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;
 
--- 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