src/Pure/Tools/debugger.scala
author wenzelm
Mon Aug 10 16:05:41 2015 +0200 (2015-08-10)
changeset 60876 52edced9cce5
parent 60875 ee23c1d21ac3
child 60878 1f0d2bbcf38b
permissions -rw-r--r--
rendering for debugger/breakpoint active state;
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@60876
    20
    active: Int = 0,
wenzelm@60876
    21
    active_breakpoints: Set[Long] = Set.empty,
wenzelm@60875
    22
    focus: Option[Position.T] = None,  // position of active GUI component
wenzelm@60842
    23
    threads: Map[String, List[Debug_State]] = Map.empty,  // thread name ~> stack of debug states
wenzelm@60834
    24
    output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
wenzelm@60834
    25
  {
wenzelm@60842
    26
    def set_session(new_session: Session): State =
wenzelm@60842
    27
      copy(session = new_session)
wenzelm@60842
    28
wenzelm@60876
    29
    def inc_active: State = copy(active = active + 1)
wenzelm@60876
    30
    def dec_active: State = copy(active = active - 1)
wenzelm@60876
    31
wenzelm@60876
    32
    def toggle_breakpoint(serial: Long): State =
wenzelm@60876
    33
    {
wenzelm@60876
    34
      val active_breakpoints1 =
wenzelm@60876
    35
        if (active_breakpoints(serial)) active_breakpoints - serial
wenzelm@60876
    36
      else active_breakpoints + serial
wenzelm@60876
    37
      copy(active_breakpoints = active_breakpoints1)
wenzelm@60876
    38
    }
wenzelm@60876
    39
wenzelm@60875
    40
    def set_focus(new_focus: Option[Position.T]): State =
wenzelm@60875
    41
      copy(focus = new_focus)
wenzelm@60875
    42
wenzelm@60842
    43
    def get_thread(thread_name: String): List[Debug_State] =
wenzelm@60842
    44
      threads.getOrElse(thread_name, Nil)
wenzelm@60842
    45
wenzelm@60842
    46
    def update_thread(thread_name: String, debug_states: List[Debug_State]): State =
wenzelm@60842
    47
      copy(threads = threads + (thread_name -> debug_states))
wenzelm@60842
    48
wenzelm@60842
    49
    def get_output(thread_name: String): Command.Results =
wenzelm@60842
    50
      output.getOrElse(thread_name, Command.Results.empty)
wenzelm@60842
    51
wenzelm@60842
    52
    def add_output(thread_name: String, entry: Command.Results.Entry): State =
wenzelm@60842
    53
      copy(output = output + (thread_name -> (get_output(thread_name) + entry)))
wenzelm@60842
    54
wenzelm@60842
    55
    def clear_output(thread_name: String): State =
wenzelm@60842
    56
      copy(output = output - thread_name)
wenzelm@60842
    57
wenzelm@60842
    58
    def purge(thread_name: String): State =
wenzelm@60842
    59
      if (get_thread(thread_name).isEmpty)
wenzelm@60842
    60
        copy(threads = threads - thread_name, output = output - thread_name)
wenzelm@60842
    61
      else this
wenzelm@60834
    62
  }
wenzelm@60834
    63
wenzelm@60834
    64
  private val global_state = Synchronized(State())
wenzelm@60834
    65
  def current_state(): State = global_state.value
wenzelm@60834
    66
wenzelm@60834
    67
wenzelm@60835
    68
  /* protocol handler */
wenzelm@60749
    69
wenzelm@60835
    70
  sealed case class Update(thread_names: Set[String])
wenzelm@60749
    71
wenzelm@60749
    72
  class Handler extends Session.Protocol_Handler
wenzelm@60749
    73
  {
wenzelm@60835
    74
    private var updated = Set.empty[String]
wenzelm@60835
    75
    private val delay_update =
wenzelm@60835
    76
      Simple_Thread.delay_first(current_state().session.output_delay) {
wenzelm@60835
    77
        current_state().session.debugger_updates.post(Update(updated))
wenzelm@60835
    78
        updated = Set.empty
wenzelm@60835
    79
      }
wenzelm@60835
    80
    private def update(name: String)
wenzelm@60835
    81
    {
wenzelm@60835
    82
      updated += name
wenzelm@60835
    83
      delay_update.invoke()
wenzelm@60835
    84
    }
wenzelm@60835
    85
wenzelm@60842
    86
    private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean =
wenzelm@60842
    87
    {
wenzelm@60842
    88
      msg.properties match {
wenzelm@60842
    89
        case Markup.Debugger_State(thread_name) =>
wenzelm@60863
    90
          val msg_body =
wenzelm@60863
    91
            YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes)))
wenzelm@60842
    92
          val debug_states =
wenzelm@60842
    93
          {
wenzelm@60842
    94
            import XML.Decode._
wenzelm@60842
    95
            list(pair(properties, Symbol.decode_string))(msg_body).map({
wenzelm@60842
    96
              case (pos, function) => Debug_State(pos, function)
wenzelm@60842
    97
            })
wenzelm@60842
    98
          }
wenzelm@60842
    99
          global_state.change(_.update_thread(thread_name, debug_states))
wenzelm@60842
   100
          update(thread_name)
wenzelm@60842
   101
          true
wenzelm@60842
   102
        case _ => false
wenzelm@60842
   103
      }
wenzelm@60842
   104
    }
wenzelm@60842
   105
wenzelm@60830
   106
    private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
wenzelm@60830
   107
    {
wenzelm@60830
   108
      msg.properties match {
wenzelm@60835
   109
        case Markup.Debugger_Output(thread_name) =>
wenzelm@60834
   110
          val msg_body =
wenzelm@60834
   111
            prover.xml_cache.body(
wenzelm@60863
   112
              YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))))
wenzelm@60834
   113
          msg_body match {
wenzelm@60834
   114
            case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
wenzelm@60834
   115
              val message = XML.Elem(Markup(Markup.message(name), props), body)
wenzelm@60835
   116
              global_state.change(_.add_output(thread_name, i -> message))
wenzelm@60835
   117
              update(thread_name)
wenzelm@60834
   118
              true
wenzelm@60834
   119
            case _ => false
wenzelm@60834
   120
          }
wenzelm@60830
   121
        case _ => false
wenzelm@60830
   122
      }
wenzelm@60830
   123
    }
wenzelm@60830
   124
wenzelm@60830
   125
    val functions =
wenzelm@60842
   126
      Map(
wenzelm@60842
   127
        Markup.DEBUGGER_STATE -> debugger_state _,
wenzelm@60842
   128
        Markup.DEBUGGER_OUTPUT -> debugger_output _)
wenzelm@60749
   129
  }
wenzelm@60765
   130
wenzelm@60765
   131
wenzelm@60765
   132
  /* protocol commands */
wenzelm@60765
   133
wenzelm@60842
   134
  def init(session: Session)
wenzelm@60835
   135
  {
wenzelm@60842
   136
    global_state.change(_.set_session(session))
wenzelm@60835
   137
    current_state().session.protocol_command("Debugger.init")
wenzelm@60835
   138
  }
wenzelm@60765
   139
wenzelm@60876
   140
  def is_active(): Boolean = current_state().active > 0
wenzelm@60876
   141
  def inc_active(): Unit = global_state.change(_.inc_active)
wenzelm@60876
   142
  def dec_active(): Unit = global_state.change(_.dec_active)
wenzelm@60876
   143
wenzelm@60876
   144
  def breakpoint_active(serial: Long): Option[Boolean] =
wenzelm@60876
   145
  {
wenzelm@60876
   146
    val state = current_state()
wenzelm@60876
   147
    if (state.active > 0) Some(state.active_breakpoints(serial)) else None
wenzelm@60876
   148
  }
wenzelm@60876
   149
wenzelm@60876
   150
  def toggle_breakpoint(serial: Long): Unit =
wenzelm@60876
   151
    global_state.change(_.toggle_breakpoint(serial))
wenzelm@60876
   152
wenzelm@60875
   153
  def focus(new_focus: Option[Position.T]): Boolean =
wenzelm@60875
   154
    global_state.change_result(state => (state.focus != new_focus, state.set_focus(new_focus)))
wenzelm@60875
   155
wenzelm@60854
   156
  def cancel(thread_name: String): Unit =
wenzelm@60854
   157
    current_state().session.protocol_command("Debugger.cancel", thread_name)
wenzelm@60765
   158
wenzelm@60854
   159
  def input(thread_name: String, msg: String*): Unit =
wenzelm@60854
   160
    current_state().session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
wenzelm@60854
   161
wenzelm@60869
   162
  def step(thread_name: String): Unit = input(thread_name, "step")
wenzelm@60869
   163
  def step_over(thread_name: String): Unit = input(thread_name, "step_over")
wenzelm@60869
   164
  def step_out(thread_name: String): Unit = input(thread_name, "step_out")
wenzelm@60854
   165
  def continue(thread_name: String): Unit = input(thread_name, "continue")
wenzelm@60856
   166
wenzelm@60857
   167
  def eval(thread_name: String, index: Int, SML: Boolean, context: String, expression: String): Unit =
wenzelm@60856
   168
  {
wenzelm@60857
   169
    input(thread_name, "eval",
wenzelm@60863
   170
      index.toString, SML.toString, Symbol.encode(context), Symbol.encode(expression))
wenzelm@60856
   171
  }
wenzelm@60749
   172
}