maintain debugger output messages;
authorwenzelm
Thu Jul 30 11:39:30 2015 +0200 (2015-07-30 ago)
changeset 60834781f1168d31e
parent 60833 d201996f72a8
child 60835 6512bb0b1ff4
maintain debugger output messages;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Tools/debugger.ML
src/Pure/Tools/debugger.scala
src/Tools/jEdit/src/debugger_dockable.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Thu Jul 30 11:32:58 2015 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Thu Jul 30 11:39:30 2015 +0200
     1.3 @@ -191,7 +191,7 @@
     1.4    val build_theories_result: string -> Properties.T
     1.5    val print_operationsN: string
     1.6    val print_operations: Properties.T
     1.7 -  val debugger_output: string -> serial -> Properties.T
     1.8 +  val debugger_output: string -> Properties.T
     1.9    val simp_trace_panelN: string
    1.10    val simp_trace_logN: string
    1.11    val simp_trace_stepN: string
    1.12 @@ -614,8 +614,7 @@
    1.13  
    1.14  (* debugger *)
    1.15  
    1.16 -fun debugger_output name i =
    1.17 -  [(functionN, "debugger_output"), (nameN, name), (serialN, print_int i)];
    1.18 +fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)];
    1.19  
    1.20  
    1.21  (* simplifier trace *)
     2.1 --- a/src/Pure/PIDE/markup.scala	Thu Jul 30 11:32:58 2015 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Thu Jul 30 11:39:30 2015 +0200
     2.3 @@ -498,10 +498,9 @@
     2.4    val DEBUGGER_OUTPUT = "debugger_output"
     2.5    object Debugger_Output
     2.6    {
     2.7 -    def unapply(props: Properties.T): Option[(String, Long)] =
     2.8 +    def unapply(props: Properties.T): Option[String] =
     2.9        props match {
    2.10 -        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name), (SERIAL, Properties.Value.Long(i))) =>
    2.11 -          Some((name, i))
    2.12 +        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
    2.13          case _ => None
    2.14        }
    2.15    }
     3.1 --- a/src/Pure/Tools/debugger.ML	Thu Jul 30 11:32:58 2015 +0200
     3.2 +++ b/src/Pure/Tools/debugger.ML	Thu Jul 30 11:39:30 2015 +0200
     3.3 @@ -6,7 +6,9 @@
     3.4  
     3.5  signature DEBUGGER =
     3.6  sig
     3.7 -  val output: string -> unit
     3.8 +  val writeln_message: string -> unit
     3.9 +  val warning_message: string -> unit
    3.10 +  val error_message: string -> unit
    3.11  end;
    3.12  
    3.13  structure Debugger: DEBUGGER =
    3.14 @@ -14,9 +16,14 @@
    3.15  
    3.16  (* messages *)
    3.17  
    3.18 -fun output msg =
    3.19 +fun output_message kind msg =
    3.20    Output.protocol_message
    3.21 -    (Markup.debugger_output (Simple_Thread.the_name ()) (serial ())) [msg];
    3.22 +    (Markup.debugger_output (Simple_Thread.the_name ()))
    3.23 +    [Markup.markup (kind, Markup.serial_properties (serial ())) msg];
    3.24 +
    3.25 +val writeln_message = output_message Markup.writelnN;
    3.26 +val warning_message = output_message Markup.warningN;
    3.27 +val error_message = output_message Markup.errorN;
    3.28  
    3.29  
    3.30  (* global state *)
     4.1 --- a/src/Pure/Tools/debugger.scala	Thu Jul 30 11:32:58 2015 +0200
     4.2 +++ b/src/Pure/Tools/debugger.scala	Thu Jul 30 11:39:30 2015 +0200
     4.3 @@ -9,6 +9,19 @@
     4.4  
     4.5  object Debugger
     4.6  {
     4.7 +  /* global state */
     4.8 +
     4.9 +  case class State(
    4.10 +    output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
    4.11 +  {
    4.12 +    def add_output(name: String, entry: Command.Results.Entry): State =
    4.13 +      copy(output = output + (name -> (output.getOrElse(name, Command.Results.empty) + entry)))
    4.14 +  }
    4.15 +
    4.16 +  private val global_state = Synchronized(State())
    4.17 +  def current_state(): State = global_state.value
    4.18 +
    4.19 +
    4.20    /* GUI interaction */
    4.21  
    4.22    case object Event
    4.23 @@ -37,10 +50,17 @@
    4.24      private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    4.25      {
    4.26        msg.properties match {
    4.27 -        case Markup.Debugger_Output(name, serial) =>
    4.28 -          // FIXME
    4.29 -          Output.writeln("debugger_output " + name + " " + serial + "\n" + msg.text)
    4.30 -          true
    4.31 +        case Markup.Debugger_Output(name) =>
    4.32 +          val msg_body =
    4.33 +            prover.xml_cache.body(
    4.34 +              YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes)))
    4.35 +          msg_body match {
    4.36 +            case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
    4.37 +              val message = XML.Elem(Markup(Markup.message(name), props), body)
    4.38 +              global_state.change(_.add_output(name, i -> message))
    4.39 +              true
    4.40 +            case _ => false
    4.41 +          }
    4.42          case _ => false
    4.43        }
    4.44      }
     5.1 --- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Jul 30 11:32:58 2015 +0200
     5.2 +++ b/src/Tools/jEdit/src/debugger_dockable.scala	Thu Jul 30 11:39:30 2015 +0200
     5.3 @@ -92,7 +92,9 @@
     5.4      GUI_Thread.require {}
     5.5  
     5.6      val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
     5.7 -    val new_output = List(XML.Text("FIXME"))
     5.8 +    val new_output =  // FIXME select by thread name
     5.9 +      (for ((_, results) <- Debugger.current_state.output; (_, tree) <- results.iterator)
    5.10 +        yield tree).toList
    5.11  
    5.12      if (new_output != current_output)
    5.13        pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))