src/Pure/Tools/debugger.scala
author wenzelm
Thu Jul 30 11:39:30 2015 +0200 (2015-07-30)
changeset 60834 781f1168d31e
parent 60830 f56e189350b2
child 60835 6512bb0b1ff4
permissions -rw-r--r--
maintain debugger output messages;
wenzelm@60749
     1
/*  Title:      Pure/Tools/debugger.scala
wenzelm@60749
     2
    Author:     Makarius
wenzelm@60749
     3
wenzelm@60749
     4
Interactive debugger for Isabelle/ML.
wenzelm@60749
     5
*/
wenzelm@60749
     6
wenzelm@60749
     7
package isabelle
wenzelm@60749
     8
wenzelm@60749
     9
wenzelm@60749
    10
object Debugger
wenzelm@60749
    11
{
wenzelm@60834
    12
  /* global state */
wenzelm@60834
    13
wenzelm@60834
    14
  case class State(
wenzelm@60834
    15
    output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
wenzelm@60834
    16
  {
wenzelm@60834
    17
    def add_output(name: String, entry: Command.Results.Entry): State =
wenzelm@60834
    18
      copy(output = output + (name -> (output.getOrElse(name, Command.Results.empty) + entry)))
wenzelm@60834
    19
  }
wenzelm@60834
    20
wenzelm@60834
    21
  private val global_state = Synchronized(State())
wenzelm@60834
    22
  def current_state(): State = global_state.value
wenzelm@60834
    23
wenzelm@60834
    24
wenzelm@60749
    25
  /* GUI interaction */
wenzelm@60749
    26
wenzelm@60749
    27
  case object Event
wenzelm@60749
    28
wenzelm@60749
    29
wenzelm@60749
    30
  /* manager thread */
wenzelm@60749
    31
wenzelm@60749
    32
  private lazy val manager: Consumer_Thread[Any] =
wenzelm@60749
    33
    Consumer_Thread.fork[Any]("Debugger.manager", daemon = true)(
wenzelm@60749
    34
      consume = (arg: Any) =>
wenzelm@60749
    35
      {
wenzelm@60749
    36
        // FIXME
wenzelm@60749
    37
        true
wenzelm@60749
    38
      },
wenzelm@60749
    39
      finish = () =>
wenzelm@60749
    40
      {
wenzelm@60749
    41
        // FIXME
wenzelm@60749
    42
      }
wenzelm@60749
    43
    )
wenzelm@60749
    44
wenzelm@60749
    45
wenzelm@60749
    46
  /* protocol handler */
wenzelm@60749
    47
wenzelm@60749
    48
  class Handler extends Session.Protocol_Handler
wenzelm@60749
    49
  {
wenzelm@60830
    50
    private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
wenzelm@60830
    51
    {
wenzelm@60830
    52
      msg.properties match {
wenzelm@60834
    53
        case Markup.Debugger_Output(name) =>
wenzelm@60834
    54
          val msg_body =
wenzelm@60834
    55
            prover.xml_cache.body(
wenzelm@60834
    56
              YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes)))
wenzelm@60834
    57
          msg_body match {
wenzelm@60834
    58
            case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
wenzelm@60834
    59
              val message = XML.Elem(Markup(Markup.message(name), props), body)
wenzelm@60834
    60
              global_state.change(_.add_output(name, i -> message))
wenzelm@60834
    61
              true
wenzelm@60834
    62
            case _ => false
wenzelm@60834
    63
          }
wenzelm@60830
    64
        case _ => false
wenzelm@60830
    65
      }
wenzelm@60830
    66
    }
wenzelm@60830
    67
wenzelm@60749
    68
    override def stop(prover: Prover)
wenzelm@60749
    69
    {
wenzelm@60749
    70
      manager.shutdown()
wenzelm@60749
    71
    }
wenzelm@60749
    72
wenzelm@60830
    73
    val functions =
wenzelm@60830
    74
      Map(Markup.DEBUGGER_OUTPUT -> debugger_output _)
wenzelm@60749
    75
  }
wenzelm@60765
    76
wenzelm@60765
    77
wenzelm@60765
    78
  /* protocol commands */
wenzelm@60765
    79
wenzelm@60765
    80
  def init(session: Session): Unit =
wenzelm@60765
    81
    session.protocol_command("Debugger.init")
wenzelm@60765
    82
wenzelm@60829
    83
  def cancel(session: Session, name: String): Unit =
wenzelm@60829
    84
    session.protocol_command("Debugger.cancel", name)
wenzelm@60765
    85
wenzelm@60829
    86
  def input(session: Session, name: String, msg: String*): Unit =
wenzelm@60829
    87
    session.protocol_command("Debugger.input", (name :: msg.toList):_*)
wenzelm@60749
    88
}