src/Pure/Tools/debugger.scala
author wenzelm
Thu Aug 06 14:28:59 2015 +0200 (2015-08-06)
changeset 60854 8f45dd297357
parent 60842 5510c8444bc4
child 60856 eb21ae05ec43
permissions -rw-r--r--
more controls;
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@60842
    14
  sealed case class Debug_State(
wenzelm@60842
    15
    pos: Position.T,
wenzelm@60842
    16
    function: String)
wenzelm@60842
    17
wenzelm@60835
    18
  sealed case class State(
wenzelm@60835
    19
    session: Session = new Session(Resources.empty),
wenzelm@60842
    20
    threads: Map[String, List[Debug_State]] = Map.empty,  // thread name ~> stack of debug states
wenzelm@60834
    21
    output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
wenzelm@60834
    22
  {
wenzelm@60842
    23
    def set_session(new_session: Session): State =
wenzelm@60842
    24
      copy(session = new_session)
wenzelm@60842
    25
wenzelm@60842
    26
    def get_thread(thread_name: String): List[Debug_State] =
wenzelm@60842
    27
      threads.getOrElse(thread_name, Nil)
wenzelm@60842
    28
wenzelm@60842
    29
    def update_thread(thread_name: String, debug_states: List[Debug_State]): State =
wenzelm@60842
    30
      copy(threads = threads + (thread_name -> debug_states))
wenzelm@60842
    31
wenzelm@60842
    32
    def get_output(thread_name: String): Command.Results =
wenzelm@60842
    33
      output.getOrElse(thread_name, Command.Results.empty)
wenzelm@60842
    34
wenzelm@60842
    35
    def add_output(thread_name: String, entry: Command.Results.Entry): State =
wenzelm@60842
    36
      copy(output = output + (thread_name -> (get_output(thread_name) + entry)))
wenzelm@60842
    37
wenzelm@60842
    38
    def clear_output(thread_name: String): State =
wenzelm@60842
    39
      copy(output = output - thread_name)
wenzelm@60842
    40
wenzelm@60842
    41
    def purge(thread_name: String): State =
wenzelm@60842
    42
      if (get_thread(thread_name).isEmpty)
wenzelm@60842
    43
        copy(threads = threads - thread_name, output = output - thread_name)
wenzelm@60842
    44
      else this
wenzelm@60834
    45
  }
wenzelm@60834
    46
wenzelm@60834
    47
  private val global_state = Synchronized(State())
wenzelm@60834
    48
  def current_state(): State = global_state.value
wenzelm@60834
    49
wenzelm@60834
    50
wenzelm@60835
    51
  /* protocol handler */
wenzelm@60749
    52
wenzelm@60835
    53
  sealed case class Update(thread_names: Set[String])
wenzelm@60749
    54
wenzelm@60749
    55
  class Handler extends Session.Protocol_Handler
wenzelm@60749
    56
  {
wenzelm@60835
    57
    private var updated = Set.empty[String]
wenzelm@60835
    58
    private val delay_update =
wenzelm@60835
    59
      Simple_Thread.delay_first(current_state().session.output_delay) {
wenzelm@60835
    60
        current_state().session.debugger_updates.post(Update(updated))
wenzelm@60835
    61
        updated = Set.empty
wenzelm@60835
    62
      }
wenzelm@60835
    63
    private def update(name: String)
wenzelm@60835
    64
    {
wenzelm@60835
    65
      updated += name
wenzelm@60835
    66
      delay_update.invoke()
wenzelm@60835
    67
    }
wenzelm@60835
    68
wenzelm@60842
    69
    private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean =
wenzelm@60842
    70
    {
wenzelm@60842
    71
      msg.properties match {
wenzelm@60842
    72
        case Markup.Debugger_State(thread_name) =>
wenzelm@60842
    73
          val msg_body = YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes))
wenzelm@60842
    74
          val debug_states =
wenzelm@60842
    75
          {
wenzelm@60842
    76
            import XML.Decode._
wenzelm@60842
    77
            list(pair(properties, Symbol.decode_string))(msg_body).map({
wenzelm@60842
    78
              case (pos, function) => Debug_State(pos, function)
wenzelm@60842
    79
            })
wenzelm@60842
    80
          }
wenzelm@60842
    81
          global_state.change(_.update_thread(thread_name, debug_states))
wenzelm@60842
    82
          update(thread_name)
wenzelm@60842
    83
          true
wenzelm@60842
    84
        case _ => false
wenzelm@60842
    85
      }
wenzelm@60842
    86
    }
wenzelm@60842
    87
wenzelm@60830
    88
    private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
wenzelm@60830
    89
    {
wenzelm@60830
    90
      msg.properties match {
wenzelm@60835
    91
        case Markup.Debugger_Output(thread_name) =>
wenzelm@60834
    92
          val msg_body =
wenzelm@60834
    93
            prover.xml_cache.body(
wenzelm@60834
    94
              YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes)))
wenzelm@60834
    95
          msg_body match {
wenzelm@60834
    96
            case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
wenzelm@60834
    97
              val message = XML.Elem(Markup(Markup.message(name), props), body)
wenzelm@60835
    98
              global_state.change(_.add_output(thread_name, i -> message))
wenzelm@60835
    99
              update(thread_name)
wenzelm@60834
   100
              true
wenzelm@60834
   101
            case _ => false
wenzelm@60834
   102
          }
wenzelm@60830
   103
        case _ => false
wenzelm@60830
   104
      }
wenzelm@60830
   105
    }
wenzelm@60830
   106
wenzelm@60830
   107
    val functions =
wenzelm@60842
   108
      Map(
wenzelm@60842
   109
        Markup.DEBUGGER_STATE -> debugger_state _,
wenzelm@60842
   110
        Markup.DEBUGGER_OUTPUT -> debugger_output _)
wenzelm@60749
   111
  }
wenzelm@60765
   112
wenzelm@60765
   113
wenzelm@60765
   114
  /* protocol commands */
wenzelm@60765
   115
wenzelm@60842
   116
  def init(session: Session)
wenzelm@60835
   117
  {
wenzelm@60842
   118
    global_state.change(_.set_session(session))
wenzelm@60835
   119
    current_state().session.protocol_command("Debugger.init")
wenzelm@60835
   120
  }
wenzelm@60765
   121
wenzelm@60854
   122
  def cancel(thread_name: String): Unit =
wenzelm@60854
   123
    current_state().session.protocol_command("Debugger.cancel", thread_name)
wenzelm@60765
   124
wenzelm@60854
   125
  def input(thread_name: String, msg: String*): Unit =
wenzelm@60854
   126
    current_state().session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
wenzelm@60854
   127
wenzelm@60854
   128
  def continue(thread_name: String): Unit = input(thread_name, "continue")
wenzelm@60749
   129
}