more explicit thread identification;

--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Tue Jul 21 14:07:06 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Tue Jul 21 14:12:45 2015 +0200
@@ -28,7 +28,8 @@
       Runtime.debugging NONE body () handle exn =>
         if Exn.is_interrupt exn then ()
         else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn),
-      Simple_Thread.attributes {stack_limit = NONE, interrupts = interrupts});
+      Simple_Thread.attributes
+        {name = "async_manager", stack_limit = NONE, interrupts = interrupts});
 
 val message_store_limit = 20
 val message_display_limit = 10

--- a/src/Pure/Concurrent/bash.ML	Tue Jul 21 14:07:06 2015 +0200
+++ b/src/Pure/Concurrent/bash.ML	Tue Jul 21 14:12:45 2015 +0200
@@ -31,7 +31,7 @@
     val _ = cleanup_files ();
 
     val system_thread =
-      Simple_Thread.fork {stack_limit = NONE, interrupts = false} (fn () =>
+      Simple_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
         Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
           let
             val _ = File.write script_path script;

--- a/src/Pure/Concurrent/event_timer.ML	Tue Jul 21 14:07:06 2015 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Tue Jul 21 14:12:45 2015 +0200
@@ -104,7 +104,9 @@
 
 fun manager_check manager =
   if is_some manager andalso Thread.isActive (the manager) then manager
-  else SOME (Simple_Thread.fork {stack_limit = NONE, interrupts = false} manager_loop);
+  else
+    SOME (Simple_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
+      manager_loop);
 
 fun shutdown () =
   uninterruptible (fn restore_attributes => fn () =>

--- a/src/Pure/Concurrent/future.ML	Tue Jul 21 14:07:06 2015 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Jul 21 14:12:45 2015 +0200
@@ -264,7 +264,7 @@
       Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
     val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit;
     val worker =
-      Simple_Thread.fork {stack_limit = stack_limit, interrupts = false}
+      Simple_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
         (fn () => worker_loop name);
   in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
   handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
@@ -366,7 +366,9 @@
  (do_shutdown := false;
   if scheduler_active () then ()
   else
-    scheduler := SOME (Simple_Thread.fork {stack_limit = NONE, interrupts = false} scheduler_loop));
+    scheduler :=
+      SOME (Simple_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
+        scheduler_loop));
 
 
 

--- a/src/Pure/Concurrent/simple_thread.ML	Tue Jul 21 14:07:06 2015 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Tue Jul 21 14:12:45 2015 +0200
@@ -7,7 +7,8 @@
 signature SIMPLE_THREAD =
 sig
   val is_self: Thread.thread -> bool
-  type params = {stack_limit: int option, interrupts: bool}
+  val identification: 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
   val join: Thread.thread -> unit
@@ -17,24 +18,52 @@
 structure Simple_Thread: SIMPLE_THREAD =
 struct
 
+(* self *)
+
 fun is_self thread = Thread.equal (Thread.self (), thread);
 
-type params = {stack_limit: int option, interrupts: bool};
+
+(* identification *)
+
+local
+  val tag = Universal.tag () : string Universal.tag;
+  val count = Counter.make ();
+in
+
+fun identification () = Thread.getLocal tag;
 
-fun attributes {stack_limit, interrupts} =
+fun set_identification name =
+  Thread.setLocal (tag, name ^ ":" ^ string_of_int (count ()));
+
+end;
+
+
+(* fork *)
+
+type params = {name: string, stack_limit: int option, interrupts: bool};
+
+fun attributes ({stack_limit, interrupts, ...}: params) =
   maximum_ml_stack stack_limit @
   (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
 
-fun fork params body =
+fun fork (params: params) body =
   Thread.fork (fn () =>
     print_exception_trace General.exnMessage tracing (fn () =>
-      body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
+      (set_identification (#name params); body ())
+        handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
     attributes params);
 
+
+(* join *)
+
 fun join thread =
   while Thread.isActive thread
   do OS.Process.sleep (seconds 0.1);
 
-fun interrupt_unsynchronized thread = Thread.interrupt thread handle Thread _ => ();
+
+(* interrupt *)
+
+fun interrupt_unsynchronized thread =
+  Thread.interrupt thread handle Thread _ => ();
 
 end;

--- a/src/Pure/System/message_channel.ML	Tue Jul 21 14:07:06 2015 +0200
+++ b/src/Pure/System/message_channel.ML	Tue Jul 21 14:12:45 2015 +0200
@@ -60,7 +60,8 @@
     let
       val mbox = Mailbox.create ();
       val thread =
-        Simple_Thread.fork {stack_limit = NONE, interrupts = false} (message_output mbox channel);
+        Simple_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
+          (message_output mbox channel);
       fun send msg = Mailbox.send mbox (SOME msg);
       fun shutdown () =
         (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread);