# HG changeset patch # User wenzelm # Date 1438249170 -7200 # Node ID 781f1168d31effd018a960826234319fda6ed518 # Parent d201996f72a89a4c396ccd788c84d53100797286 maintain debugger output messages; diff -r d201996f72a8 -r 781f1168d31e src/Pure/PIDE/markup.ML --- 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 *) diff -r d201996f72a8 -r 781f1168d31e src/Pure/PIDE/markup.scala --- 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 } } diff -r d201996f72a8 -r 781f1168d31e src/Pure/Tools/debugger.ML --- 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 *) diff -r d201996f72a8 -r 781f1168d31e src/Pure/Tools/debugger.scala --- 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 } } diff -r d201996f72a8 -r 781f1168d31e src/Tools/jEdit/src/debugger_dockable.scala --- 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))