src/Pure/Tools/debugger.scala
author wenzelm
Sat Aug 08 21:33:11 2015 +0200 (2015-08-08)
changeset 60869 878e32cf3131
parent 60863 21d70681ec05
child 60875 ee23c1d21ac3
permissions -rw-r--r--
more single stepping;
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@60863
    73
          val msg_body =
wenzelm@60863
    74
            YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes)))
wenzelm@60842
    75
          val debug_states =
wenzelm@60842
    76
          {
wenzelm@60842
    77
            import XML.Decode._
wenzelm@60842
    78
            list(pair(properties, Symbol.decode_string))(msg_body).map({
wenzelm@60842
    79
              case (pos, function) => Debug_State(pos, function)
wenzelm@60842
    80
            })
wenzelm@60842
    81
          }
wenzelm@60842
    82
          global_state.change(_.update_thread(thread_name, debug_states))
wenzelm@60842
    83
          update(thread_name)
wenzelm@60842
    84
          true
wenzelm@60842
    85
        case _ => false
wenzelm@60842
    86
      }
wenzelm@60842
    87
    }
wenzelm@60842
    88
wenzelm@60830
    89
    private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
wenzelm@60830
    90
    {
wenzelm@60830
    91
      msg.properties match {
wenzelm@60835
    92
        case Markup.Debugger_Output(thread_name) =>
wenzelm@60834
    93
          val msg_body =
wenzelm@60834
    94
            prover.xml_cache.body(
wenzelm@60863
    95
              YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))))
wenzelm@60834
    96
          msg_body match {
wenzelm@60834
    97
            case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
wenzelm@60834
    98
              val message = XML.Elem(Markup(Markup.message(name), props), body)
wenzelm@60835
    99
              global_state.change(_.add_output(thread_name, i -> message))
wenzelm@60835
   100
              update(thread_name)
wenzelm@60834
   101
              true
wenzelm@60834
   102
            case _ => false
wenzelm@60834
   103
          }
wenzelm@60830
   104
        case _ => false
wenzelm@60830
   105
      }
wenzelm@60830
   106
    }
wenzelm@60830
   107
wenzelm@60830
   108
    val functions =
wenzelm@60842
   109
      Map(
wenzelm@60842
   110
        Markup.DEBUGGER_STATE -> debugger_state _,
wenzelm@60842
   111
        Markup.DEBUGGER_OUTPUT -> debugger_output _)
wenzelm@60749
   112
  }
wenzelm@60765
   113
wenzelm@60765
   114
wenzelm@60765
   115
  /* protocol commands */
wenzelm@60765
   116
wenzelm@60842
   117
  def init(session: Session)
wenzelm@60835
   118
  {
wenzelm@60842
   119
    global_state.change(_.set_session(session))
wenzelm@60835
   120
    current_state().session.protocol_command("Debugger.init")
wenzelm@60835
   121
  }
wenzelm@60765
   122
wenzelm@60854
   123
  def cancel(thread_name: String): Unit =
wenzelm@60854
   124
    current_state().session.protocol_command("Debugger.cancel", thread_name)
wenzelm@60765
   125
wenzelm@60854
   126
  def input(thread_name: String, msg: String*): Unit =
wenzelm@60854
   127
    current_state().session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
wenzelm@60854
   128
wenzelm@60869
   129
  def step(thread_name: String): Unit = input(thread_name, "step")
wenzelm@60869
   130
  def step_over(thread_name: String): Unit = input(thread_name, "step_over")
wenzelm@60869
   131
  def step_out(thread_name: String): Unit = input(thread_name, "step_out")
wenzelm@60854
   132
  def continue(thread_name: String): Unit = input(thread_name, "continue")
wenzelm@60856
   133
wenzelm@60857
   134
  def eval(thread_name: String, index: Int, SML: Boolean, context: String, expression: String): Unit =
wenzelm@60856
   135
  {
wenzelm@60857
   136
    input(thread_name, "eval",
wenzelm@60863
   137
      index.toString, SML.toString, Symbol.encode(context), Symbol.encode(expression))
wenzelm@60856
   138
  }
wenzelm@60749
   139
}