# HG changeset patch
# User wenzelm
# Date 1438162886 -7200
# Node ID 4b16b778ce0db8bf51a1d29107bfc36e59dcc28f
# Parent  31e08fe243f14e20b57479c744fcfc41d3ec2cdd
clarified thread name;

diff -r 31e08fe243f1 -r 4b16b778ce0d src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Tue Jul 28 23:29:13 2015 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Wed Jul 29 11:41:26 2015 +0200
@@ -7,7 +7,7 @@
 signature SIMPLE_THREAD =
 sig
   val is_self: Thread.thread -> bool
-  val identification: unit -> string option
+  val name: unit -> string option
   type params = {name: string, stack_limit: int option, interrupts: bool}
   val attributes: params -> Thread.threadAttribute list
   val fork: params -> (unit -> unit) -> Thread.thread
@@ -23,17 +23,15 @@
 fun is_self thread = Thread.equal (Thread.self (), thread);
 
 
-(* identification *)
+(* unique name *)
 
 local
   val tag = Universal.tag () : string Universal.tag;
   val count = Counter.make ();
 in
 
-fun identification () = Thread.getLocal tag;
-
-fun set_identification name =
-  Thread.setLocal (tag, name ^ ":" ^ string_of_int (count ()));
+fun name () = Thread.getLocal tag;
+fun set_name base = Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
 
 end;
 
@@ -49,7 +47,7 @@
 fun fork (params: params) body =
   Thread.fork (fn () =>
     print_exception_trace General.exnMessage tracing (fn () =>
-      (set_identification (#name params); body ())
+      (set_name (#name params); body ())
         handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
     attributes params);
 
diff -r 31e08fe243f1 -r 4b16b778ce0d src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Tue Jul 28 23:29:13 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Wed Jul 29 11:41:26 2015 +0200
@@ -11,8 +11,8 @@
 
 datatype state =
   State of {
-    threads: Thread.thread Symtab.table,  (*thread identification ~> thread*)
-    input: string list Queue.T Symtab.table  (*thread identification ~> input queue*)
+    threads: Thread.thread Symtab.table,  (*thread name ~> thread*)
+    input: string list Queue.T Symtab.table  (*thread name ~> input queue*)
   };
 
 fun make_state (threads, input) = State {threads = threads, input = input};
@@ -21,27 +21,27 @@
 
 val global_state = Synchronized.var "Debugger.state" init_state;
 
-fun cancel id =
+fun cancel name =
   Synchronized.change global_state (tap (fn State {threads, ...} =>
-    (case Symtab.lookup threads id of
+    (case Symtab.lookup threads name of
       NONE => ()
     | SOME thread => Simple_Thread.interrupt_unsynchronized thread)));
 
-fun input id msg =
+fun input name msg =
   Synchronized.change global_state (map_state (fn (threads, input) =>
-    let val input' = Symtab.map_default (id, Queue.empty) (Queue.enqueue msg) input;
+    let val input' = Symtab.map_default (name, Queue.empty) (Queue.enqueue msg) input;
     in (threads, input') end));
 
-fun get_input id =
+fun get_input name =
   Synchronized.guarded_access global_state (fn State {threads, input} =>
-    (case Symtab.lookup input id of
+    (case Symtab.lookup input name of
       NONE => NONE
     | SOME queue =>
         let
           val (msg, queue') = Queue.dequeue queue;
           val input' =
-            if Queue.is_empty queue' then Symtab.delete_safe id input
-            else Symtab.update (id, queue') input;
+            if Queue.is_empty queue' then Symtab.delete_safe name input
+            else Symtab.update (name, queue') input;
         in SOME (msg, make_state (threads, input')) end));
 
 
@@ -65,13 +65,13 @@
 
 (* main entry point *)
 
-fun debug_loop id =
-  (case get_input id of
+fun debug_loop name =
+  (case get_input name of
     ["continue"] => ()
   | bad =>
      (Output.system_message
         ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad);
-      debug_loop id));
+      debug_loop name));
 
 fun debugger cond =
   if debugging () orelse not (cond ()) orelse
@@ -79,9 +79,9 @@
   then ()
   else
     with_debugging (fn () =>
-      (case Simple_Thread.identification () of
+      (case Simple_Thread.name () of
         NONE => ()
-      | SOME id => debug_loop id));
+      | SOME name => debug_loop name));
 
 fun init () =
   ML_Debugger.on_breakpoint
@@ -97,10 +97,10 @@
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.cancel"
-    (fn [id] => cancel id);
+    (fn [name] => cancel name);
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.input"
-    (fn id :: msg => input id msg);
+    (fn name :: msg => input name msg);
 
 end;
diff -r 31e08fe243f1 -r 4b16b778ce0d src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Tue Jul 28 23:29:13 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Wed Jul 29 11:41:26 2015 +0200
@@ -48,9 +48,9 @@
   def init(session: Session): Unit =
     session.protocol_command("Debugger.init")
 
-  def cancel(session: Session, id: String): Unit =
-    session.protocol_command("Debugger.cancel", id)
+  def cancel(session: Session, name: String): Unit =
+    session.protocol_command("Debugger.cancel", name)
 
-  def input(session: Session, id: String, msg: String*): Unit =
-    session.protocol_command("Debugger.input", (id :: msg.toList):_*)
+  def input(session: Session, name: String, msg: String*): Unit =
+    session.protocol_command("Debugger.input", (name :: msg.toList):_*)
 }