maintain debugger output messages;

--- a/src/Pure/PIDE/markup.ML	Thu Jul 30 11:32:58 2015 +0200
+++ b/src/Pure/PIDE/markup.ML	Thu Jul 30 11:39:30 2015 +0200
@@ -191,7 +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 debugger_output: string -> Properties.T
   val simp_trace_panelN: string
   val simp_trace_logN: string
   val simp_trace_stepN: string
@@ -614,8 +614,7 @@
 
 (* debugger *)
 
-fun debugger_output name i =
-  [(functionN, "debugger_output"), (nameN, name), (serialN, print_int i)];
+fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)];
 
 
 (* simplifier trace *)

--- a/src/Pure/PIDE/markup.scala	Thu Jul 30 11:32:58 2015 +0200
+++ b/src/Pure/PIDE/markup.scala	Thu Jul 30 11:39:30 2015 +0200
@@ -498,10 +498,9 @@
   val DEBUGGER_OUTPUT = "debugger_output"
   object Debugger_Output
   {
-    def unapply(props: Properties.T): Option[(String, Long)] =
+    def unapply(props: Properties.T): Option[String] =
       props match {
-        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name), (SERIAL, Properties.Value.Long(i))) =>
-          Some((name, i))
+        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
         case _ => None
       }
   }

--- a/src/Pure/Tools/debugger.ML	Thu Jul 30 11:32:58 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Thu Jul 30 11:39:30 2015 +0200
@@ -6,7 +6,9 @@
 
 signature DEBUGGER =
 sig
-  val output: string -> unit
+  val writeln_message: string -> unit
+  val warning_message: string -> unit
+  val error_message: string -> unit
 end;
 
 structure Debugger: DEBUGGER =
@@ -14,9 +16,14 @@
 
 (* messages *)
 
-fun output msg =
+fun output_message kind msg =
   Output.protocol_message
-    (Markup.debugger_output (Simple_Thread.the_name ()) (serial ())) [msg];
+    (Markup.debugger_output (Simple_Thread.the_name ()))
+    [Markup.markup (kind, Markup.serial_properties (serial ())) msg];
+
+val writeln_message = output_message Markup.writelnN;
+val warning_message = output_message Markup.warningN;
+val error_message = output_message Markup.errorN;
 
 
 (* global state *)

--- a/src/Pure/Tools/debugger.scala	Thu Jul 30 11:32:58 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Thu Jul 30 11:39:30 2015 +0200
@@ -9,6 +9,19 @@
 
 object Debugger
 {
+  /* global state */
+
+  case class State(
+    output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
+  {
+    def add_output(name: String, entry: Command.Results.Entry): State =
+      copy(output = output + (name -> (output.getOrElse(name, Command.Results.empty) + entry)))
+  }
+
+  private val global_state = Synchronized(State())
+  def current_state(): State = global_state.value
+
+
   /* GUI interaction */
 
   case object Event
@@ -37,10 +50,17 @@
     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 Markup.Debugger_Output(name) =>
+          val msg_body =
+            prover.xml_cache.body(
+              YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes)))
+          msg_body match {
+            case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
+              val message = XML.Elem(Markup(Markup.message(name), props), body)
+              global_state.change(_.add_output(name, i -> message))
+              true
+            case _ => false
+          }
         case _ => false
       }
     }

--- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Jul 30 11:32:58 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Thu Jul 30 11:39:30 2015 +0200
@@ -92,7 +92,9 @@
     GUI_Thread.require {}
 
     val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
-    val new_output = List(XML.Text("FIXME"))
+    val new_output =  // FIXME select by thread name
+      (for ((_, results) <- Debugger.current_state.output; (_, tree) <- results.iterator)
+        yield tree).toList
 
     if (new_output != current_output)
       pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))