# HG changeset patch
# User wenzelm
# Date 1586085852 -7200
# Node ID 16aa085f935330f4f93403f94b7caef929fead7e
# Parent  f249b5c0fea221b363834f9e7d63b8ebdea09ab2
clarified signature: more uniform ML vs. Scala;

diff -r f249b5c0fea2 -r 16aa085f9353 src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Sun Apr 05 13:19:29 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Sun Apr 05 13:24:12 2020 +0200
@@ -7,8 +7,7 @@
 signature ISABELLE_THREAD =
 sig
   val is_self: Thread.thread -> bool
-  val get_name: unit -> string option
-  val the_name: unit -> string
+  val get_name: unit -> string
   type params = {name: string, stack_limit: int option, interrupts: bool}
   val attributes: params -> Thread.threadAttribute list
   val fork: params -> (unit -> unit) -> Thread.thread
@@ -31,12 +30,10 @@
   val count = Counter.make ();
 in
 
-fun get_name () = Thread_Data.get name_var;
-
-fun the_name () =
-  (case get_name () of
-    NONE => raise Fail "Unknown thread name"
-  | SOME name => name);
+fun get_name () =
+  (case Thread_Data.get name_var of
+    SOME name => name
+  | NONE => raise Fail "Isabelle-specific thread required");
 
 fun set_name base =
   Thread_Data.put name_var (SOME ("Isabelle." ^ base ^ "-" ^ string_of_int (count ())));
diff -r f249b5c0fea2 -r 16aa085f9353 src/Pure/Concurrent/isabelle_thread.scala
--- a/src/Pure/Concurrent/isabelle_thread.scala	Sun Apr 05 13:19:29 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.scala	Sun Apr 05 13:24:12 2020 +0200
@@ -45,7 +45,7 @@
   def self: Isabelle_Thread =
     Thread.currentThread match {
       case thread: Isabelle_Thread => thread
-      case _ => error("Expected to run on Isabelle/Scala standard thread")
+      case _ => error("Isabelle-specific thread required")
     }
 
   def uninterruptible[A](body: => A): A = self.uninterruptible(body)
diff -r f249b5c0fea2 -r 16aa085f9353 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Sun Apr 05 13:19:29 2020 +0200
+++ b/src/Pure/Tools/debugger.ML	Sun Apr 05 13:24:12 2020 +0200
@@ -22,7 +22,7 @@
   if msg = "" then ()
   else
     Output.protocol_message
-      (Markup.debugger_output (Isabelle_Thread.the_name ()))
+      (Markup.debugger_output (Isabelle_Thread.get_name ()))
       [XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)];
 
 val writeln_message = output_message Markup.writelnN;
@@ -250,7 +250,7 @@
         (SOME (fn (_, break) =>
           if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
           then
-            (case Isabelle_Thread.get_name () of
+            (case try Isabelle_Thread.get_name () of
               SOME thread_name => debugger_loop thread_name
             | NONE => ())
           else ()))));