separate channel for debugger output;
clarified thread name;

--- a/src/Pure/Concurrent/simple_thread.ML	Wed Jul 29 11:41:26 2015 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Wed Jul 29 13:34:04 2015 +0200
@@ -7,7 +7,8 @@
 signature SIMPLE_THREAD =
 sig
   val is_self: Thread.thread -> bool
-  val name: unit -> string option
+  val get_name: unit -> string option
+  val the_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
@@ -30,8 +31,15 @@
   val count = Counter.make ();
 in
 
-fun name () = Thread.getLocal tag;
-fun set_name base = Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
+fun get_name () = Thread.getLocal tag;
+
+fun the_name () =
+  (case get_name () of
+    NONE => raise Fail "Unknown thread name"
+  | SOME name => name);
+
+fun set_name base =
+  Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
 
 end;
 

--- a/src/Pure/PIDE/markup.ML	Wed Jul 29 11:41:26 2015 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Jul 29 13:34:04 2015 +0200
@@ -191,6 +191,7 @@
   val build_theories_result: string -> Properties.T
   val print_operationsN: string
   val print_operations: Properties.T
+  val debugger_output: string -> serial -> Properties.T
   val simp_trace_panelN: string
   val simp_trace_logN: string
   val simp_trace_stepN: string
@@ -611,6 +612,12 @@
 val print_operations = [(functionN, print_operationsN)];
 
 
+(* debugger *)
+
+fun debugger_output name i =
+  [(functionN, "debugger_output"), (nameN, name), (serialN, print_int i)];
+
+
 (* simplifier trace *)
 
 val simp_trace_panelN = "simp_trace_panel";

--- a/src/Pure/PIDE/markup.scala	Wed Jul 29 11:41:26 2015 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Jul 29 13:34:04 2015 +0200
@@ -493,6 +493,20 @@
   val PRINT_OPERATIONS = "print_operations"
 
 
+  /* debugger output */
+
+  val DEBUGGER_OUTPUT = "debugger_output"
+  object Debugger_Output
+  {
+    def unapply(props: Properties.T): Option[(String, Long)] =
+      props match {
+        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name), (SERIAL, Properties.Value.Long(i))) =>
+          Some((name, i))
+        case _ => None
+      }
+  }
+
+
   /* simplifier trace */
 
   val SIMP_TRACE_PANEL = "simp_trace_panel"

--- a/src/Pure/Tools/debugger.ML	Wed Jul 29 11:41:26 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Wed Jul 29 13:34:04 2015 +0200
@@ -4,9 +4,21 @@
 Interactive debugger for Isabelle/ML.
 *)
 
-structure Debugger: sig end =
+signature DEBUGGER =
+sig
+  val output: string -> unit
+end;
+
+structure Debugger: DEBUGGER =
 struct
 
+(* messages *)
+
+fun output msg =
+  Output.protocol_message
+    (Markup.debugger_output (Simple_Thread.the_name ()) (serial ())) [msg];
+
+
 (* global state *)
 
 datatype state =
@@ -79,7 +91,7 @@
   then ()
   else
     with_debugging (fn () =>
-      (case Simple_Thread.name () of
+      (case Simple_Thread.get_name () of
         NONE => ()
       | SOME name => debug_loop name));
 

--- a/src/Pure/Tools/debugger.scala	Wed Jul 29 11:41:26 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Wed Jul 29 13:34:04 2015 +0200
@@ -34,12 +34,24 @@
 
   class Handler extends Session.Protocol_Handler
   {
+    private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+    {
+      msg.properties match {
+        case Markup.Debugger_Output(name, serial) =>
+          // FIXME
+          Output.writeln("debugger_output " + name + " " + serial + "\n" + msg.text)
+          true
+        case _ => false
+      }
+    }
+
     override def stop(prover: Prover)
     {
       manager.shutdown()
     }
 
-    val functions = Map.empty[String, (Prover, Prover.Protocol_Output) => Boolean]  // FIXME
+    val functions =
+      Map(Markup.DEBUGGER_OUTPUT -> debugger_output _)
   }