--- 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 ())));