src/Pure/Tools/debugger.scala
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (21 months ago)
changeset 66822 4642cf4a7ebb
parent 65344 b99283eed13c
permissions -rw-r--r--
tuned signature;
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@61016
    10
import scala.collection.immutable.SortedMap
wenzelm@61016
    11
wenzelm@61016
    12
wenzelm@60749
    13
object Debugger
wenzelm@60749
    14
{
wenzelm@65213
    15
  /* thread context */
wenzelm@60834
    16
wenzelm@65213
    17
  case object Update
wenzelm@65213
    18
wenzelm@65213
    19
  sealed case class Debug_State(pos: Position.T, function: String)
wenzelm@65213
    20
  type Threads = SortedMap[String, List[Debug_State]]
wenzelm@60842
    21
wenzelm@61010
    22
  sealed case class Context(thread_name: String, debug_states: List[Debug_State], index: Int = 0)
wenzelm@61010
    23
  {
wenzelm@61010
    24
    def size: Int = debug_states.length + 1
wenzelm@61010
    25
    def reset: Context = copy(index = 0)
wenzelm@61010
    26
    def select(i: Int) = copy(index = i + 1)
wenzelm@61010
    27
wenzelm@61010
    28
    def thread_state: Option[Debug_State] = debug_states.headOption
wenzelm@61010
    29
wenzelm@61010
    30
    def stack_state: Option[Debug_State] =
wenzelm@61010
    31
      if (1 <= index && index <= debug_states.length)
wenzelm@61010
    32
        Some(debug_states(index - 1))
wenzelm@61010
    33
      else None
wenzelm@61010
    34
wenzelm@61014
    35
    def debug_index: Option[Int] =
wenzelm@61010
    36
      if (stack_state.isDefined) Some(index - 1)
wenzelm@61010
    37
      else if (debug_states.nonEmpty) Some(0)
wenzelm@61010
    38
      else None
wenzelm@61010
    39
wenzelm@61010
    40
    def debug_state: Option[Debug_State] = stack_state orElse thread_state
wenzelm@61014
    41
    def debug_position: Option[Position.T] = debug_state.map(_.pos)
wenzelm@61010
    42
wenzelm@61010
    43
    override def toString: String =
wenzelm@61010
    44
      stack_state match {
wenzelm@61010
    45
        case None => thread_name
wenzelm@61010
    46
        case Some(d) => d.function
wenzelm@61010
    47
      }
wenzelm@61010
    48
  }
wenzelm@61010
    49
wenzelm@61010
    50
wenzelm@65213
    51
  /* debugger state */
wenzelm@61016
    52
wenzelm@60835
    53
  sealed case class State(
wenzelm@60932
    54
    active: Int = 0,  // active views
wenzelm@60932
    55
    break: Boolean = false,  // break at next possible breakpoint
wenzelm@60932
    56
    active_breakpoints: Set[Long] = Set.empty,  // explicit breakpoint state
wenzelm@61016
    57
    threads: Threads = SortedMap.empty,  // thread name ~> stack of debug states
wenzelm@61014
    58
    focus: Map[String, Context] = Map.empty,  // thread name ~> focus
wenzelm@60834
    59
    output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
wenzelm@60834
    60
  {
wenzelm@60932
    61
    def set_break(b: Boolean): State = copy(break = b)
wenzelm@60932
    62
wenzelm@65223
    63
    def is_active: Boolean = active > 0
wenzelm@60898
    64
    def inc_active: State = copy(active = active + 1)
wenzelm@60898
    65
    def dec_active: State = copy(active = active - 1)
wenzelm@60876
    66
wenzelm@60880
    67
    def toggle_breakpoint(breakpoint: Long): (Boolean, State) =
wenzelm@60876
    68
    {
wenzelm@60876
    69
      val active_breakpoints1 =
wenzelm@60880
    70
        if (active_breakpoints(breakpoint)) active_breakpoints - breakpoint
wenzelm@60880
    71
      else active_breakpoints + breakpoint
wenzelm@60880
    72
      (active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1))
wenzelm@60876
    73
    }
wenzelm@60876
    74
wenzelm@60842
    75
    def get_thread(thread_name: String): List[Debug_State] =
wenzelm@60842
    76
      threads.getOrElse(thread_name, Nil)
wenzelm@60842
    77
wenzelm@60842
    78
    def update_thread(thread_name: String, debug_states: List[Debug_State]): State =
wenzelm@61019
    79
    {
wenzelm@61019
    80
      val threads1 =
wenzelm@61019
    81
        if (debug_states.nonEmpty) threads + (thread_name -> debug_states)
wenzelm@61019
    82
        else threads - thread_name
wenzelm@61019
    83
      val focus1 =
wenzelm@61019
    84
        focus.get(thread_name) match {
wenzelm@61019
    85
          case Some(c) if debug_states.nonEmpty =>
wenzelm@61019
    86
            focus + (thread_name -> Context(thread_name, debug_states))
wenzelm@61019
    87
          case _ => focus - thread_name
wenzelm@61019
    88
        }
wenzelm@61019
    89
      copy(threads = threads1, focus = focus1)
wenzelm@61019
    90
    }
wenzelm@60842
    91
wenzelm@61014
    92
    def set_focus(c: Context): State = copy(focus = focus + (c.thread_name -> c))
wenzelm@61014
    93
wenzelm@60842
    94
    def get_output(thread_name: String): Command.Results =
wenzelm@60842
    95
      output.getOrElse(thread_name, Command.Results.empty)
wenzelm@60842
    96
wenzelm@60842
    97
    def add_output(thread_name: String, entry: Command.Results.Entry): State =
wenzelm@60842
    98
      copy(output = output + (thread_name -> (get_output(thread_name) + entry)))
wenzelm@60842
    99
wenzelm@60842
   100
    def clear_output(thread_name: String): State =
wenzelm@60842
   101
      copy(output = output - thread_name)
wenzelm@60834
   102
  }
wenzelm@60834
   103
wenzelm@60902
   104
wenzelm@60902
   105
  /* protocol handler */
wenzelm@60902
   106
wenzelm@65222
   107
  class Handler(session: Session) extends Session.Protocol_Handler
wenzelm@60749
   108
  {
wenzelm@65222
   109
    val debugger: Debugger = new Debugger(session)
wenzelm@65213
   110
wenzelm@65219
   111
    private def debugger_state(msg: Prover.Protocol_Output): Boolean =
wenzelm@60842
   112
    {
wenzelm@60842
   113
      msg.properties match {
wenzelm@60842
   114
        case Markup.Debugger_State(thread_name) =>
wenzelm@65344
   115
          val msg_body = Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes))
wenzelm@60842
   116
          val debug_states =
wenzelm@60842
   117
          {
wenzelm@60842
   118
            import XML.Decode._
wenzelm@65344
   119
            list(pair(properties, string))(msg_body).map({
wenzelm@60842
   120
              case (pos, function) => Debug_State(pos, function)
wenzelm@60842
   121
            })
wenzelm@60842
   122
          }
wenzelm@65222
   123
          debugger.update_thread(thread_name, debug_states)
wenzelm@60842
   124
          true
wenzelm@60842
   125
        case _ => false
wenzelm@60842
   126
      }
wenzelm@60842
   127
    }
wenzelm@60842
   128
wenzelm@65219
   129
    private def debugger_output(msg: Prover.Protocol_Output): Boolean =
wenzelm@60830
   130
    {
wenzelm@60830
   131
      msg.properties match {
wenzelm@60835
   132
        case Markup.Debugger_Output(thread_name) =>
wenzelm@65344
   133
          Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) match {
wenzelm@60834
   134
            case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
wenzelm@65218
   135
              val message = XML.Elem(Markup(Markup.message(name), props), body)
wenzelm@65222
   136
              debugger.add_output(thread_name, i -> session.xml_cache.elem(message))
wenzelm@60834
   137
              true
wenzelm@60834
   138
            case _ => false
wenzelm@60834
   139
          }
wenzelm@60830
   140
        case _ => false
wenzelm@60830
   141
      }
wenzelm@60830
   142
    }
wenzelm@60830
   143
wenzelm@60830
   144
    val functions =
wenzelm@65219
   145
      List(
wenzelm@60842
   146
        Markup.DEBUGGER_STATE -> debugger_state _,
wenzelm@60842
   147
        Markup.DEBUGGER_OUTPUT -> debugger_output _)
wenzelm@60749
   148
  }
wenzelm@65213
   149
}
wenzelm@65213
   150
wenzelm@65222
   151
class Debugger private(session: Session)
wenzelm@65213
   152
{
wenzelm@65213
   153
  /* debugger state */
wenzelm@65213
   154
wenzelm@65223
   155
  private val state = Synchronized(Debugger.State())
wenzelm@65213
   156
wenzelm@65213
   157
  private val delay_update =
wenzelm@65213
   158
    Standard_Thread.delay_first(session.output_delay) {
wenzelm@65213
   159
      session.debugger_updates.post(Debugger.Update)
wenzelm@65213
   160
    }
wenzelm@60765
   161
wenzelm@60765
   162
wenzelm@60765
   163
  /* protocol commands */
wenzelm@60765
   164
wenzelm@65213
   165
  def update_thread(thread_name: String, debug_states: List[Debugger.Debug_State])
wenzelm@60910
   166
  {
wenzelm@65213
   167
    state.change(_.update_thread(thread_name, debug_states))
wenzelm@65213
   168
    delay_update.invoke()
wenzelm@60910
   169
  }
wenzelm@60910
   170
wenzelm@65213
   171
  def add_output(thread_name: String, entry: Command.Results.Entry)
wenzelm@65213
   172
  {
wenzelm@65213
   173
    state.change(_.add_output(thread_name, entry))
wenzelm@65213
   174
    delay_update.invoke()
wenzelm@65213
   175
  }
wenzelm@65213
   176
wenzelm@65223
   177
  def is_active(): Boolean = session.is_ready && state.value.is_active
wenzelm@65223
   178
wenzelm@65223
   179
  def ready()
wenzelm@65223
   180
  {
wenzelm@65223
   181
    if (is_active())
wenzelm@65223
   182
      session.protocol_command("Debugger.init")
wenzelm@65223
   183
  }
wenzelm@65213
   184
wenzelm@60910
   185
  def init(): Unit =
wenzelm@65213
   186
    state.change(st =>
wenzelm@60889
   187
    {
wenzelm@65213
   188
      val st1 = st.inc_active
wenzelm@65223
   189
      if (session.is_ready && !st.is_active && st1.is_active)
wenzelm@65213
   190
        session.protocol_command("Debugger.init")
wenzelm@65213
   191
      st1
wenzelm@60889
   192
    })
wenzelm@60889
   193
wenzelm@60910
   194
  def exit(): Unit =
wenzelm@65213
   195
    state.change(st =>
wenzelm@60889
   196
    {
wenzelm@65213
   197
      val st1 = st.dec_active
wenzelm@65223
   198
      if (session.is_ready && st.is_active && !st1.is_active)
wenzelm@65213
   199
        session.protocol_command("Debugger.exit")
wenzelm@65213
   200
      st1
wenzelm@60889
   201
    })
wenzelm@60876
   202
wenzelm@65213
   203
  def is_break(): Boolean = state.value.break
wenzelm@60932
   204
  def set_break(b: Boolean)
wenzelm@60932
   205
  {
wenzelm@65213
   206
    state.change(st => {
wenzelm@65213
   207
      val st1 = st.set_break(b)
wenzelm@65213
   208
      session.protocol_command("Debugger.break", b.toString)
wenzelm@65213
   209
      st1
wenzelm@60932
   210
    })
wenzelm@60932
   211
    delay_update.invoke()
wenzelm@60932
   212
  }
wenzelm@60932
   213
wenzelm@60882
   214
  def active_breakpoint_state(breakpoint: Long): Option[Boolean] =
wenzelm@60876
   215
  {
wenzelm@65213
   216
    val st = state.value
wenzelm@65213
   217
    if (st.is_active) Some(st.active_breakpoints(breakpoint)) else None
wenzelm@60876
   218
  }
wenzelm@60876
   219
wenzelm@60882
   220
  def breakpoint_state(breakpoint: Long): Boolean =
wenzelm@65213
   221
    state.value.active_breakpoints(breakpoint)
wenzelm@60882
   222
wenzelm@60880
   223
  def toggle_breakpoint(command: Command, breakpoint: Long)
wenzelm@60878
   224
  {
wenzelm@65213
   225
    state.change(st =>
wenzelm@65213
   226
      {
wenzelm@65213
   227
        val (breakpoint_state, st1) = st.toggle_breakpoint(breakpoint)
wenzelm@65213
   228
        session.protocol_command(
wenzelm@65213
   229
          "Debugger.breakpoint",
wenzelm@65213
   230
          Symbol.encode(command.node_name.node),
wenzelm@65213
   231
          Document_ID(command.id),
wenzelm@65213
   232
          Value.Long(breakpoint),
wenzelm@65213
   233
          Value.Boolean(breakpoint_state))
wenzelm@65213
   234
        st1
wenzelm@65213
   235
      })
wenzelm@60878
   236
  }
wenzelm@60876
   237
wenzelm@65213
   238
  def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Tree]) =
wenzelm@61018
   239
  {
wenzelm@65213
   240
    val st = state.value
wenzelm@61018
   241
    val output =
wenzelm@61018
   242
      focus match {
wenzelm@61018
   243
        case None => Nil
wenzelm@61018
   244
        case Some(c) =>
wenzelm@61018
   245
          (for {
wenzelm@65213
   246
            (thread_name, results) <- st.output
wenzelm@61018
   247
            if thread_name == c.thread_name
wenzelm@61018
   248
            (_, tree) <- results.iterator
wenzelm@61018
   249
          } yield tree).toList
wenzelm@61018
   250
      }
wenzelm@65213
   251
    (st.threads, output)
wenzelm@61018
   252
  }
wenzelm@61011
   253
wenzelm@65213
   254
  def focus(): List[Debugger.Context] = state.value.focus.toList.map(_._2)
wenzelm@65213
   255
  def set_focus(c: Debugger.Context)
wenzelm@61008
   256
  {
wenzelm@65213
   257
    state.change(_.set_focus(c))
wenzelm@61008
   258
    delay_update.invoke()
wenzelm@61008
   259
  }
wenzelm@60875
   260
wenzelm@60854
   261
  def input(thread_name: String, msg: String*): Unit =
wenzelm@65213
   262
    session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
wenzelm@60854
   263
wenzelm@60899
   264
  def continue(thread_name: String): Unit = input(thread_name, "continue")
wenzelm@60869
   265
  def step(thread_name: String): Unit = input(thread_name, "step")
wenzelm@60869
   266
  def step_over(thread_name: String): Unit = input(thread_name, "step_over")
wenzelm@60869
   267
  def step_out(thread_name: String): Unit = input(thread_name, "step_out")
wenzelm@60856
   268
wenzelm@60901
   269
  def clear_output(thread_name: String)
wenzelm@60901
   270
  {
wenzelm@65213
   271
    state.change(_.clear_output(thread_name))
wenzelm@60902
   272
    delay_update.invoke()
wenzelm@60901
   273
  }
wenzelm@60901
   274
wenzelm@65213
   275
  def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String)
wenzelm@60856
   276
  {
wenzelm@65213
   277
    state.change(st => {
wenzelm@61014
   278
      input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString,
wenzelm@61010
   279
        SML.toString, Symbol.encode(context), Symbol.encode(expression))
wenzelm@65213
   280
      st.clear_output(c.thread_name)
wenzelm@60896
   281
    })
wenzelm@60902
   282
    delay_update.invoke()
wenzelm@60856
   283
  }
wenzelm@60897
   284
wenzelm@65213
   285
  def print_vals(c: Debugger.Context, SML: Boolean, context: String)
wenzelm@60897
   286
  {
wenzelm@61014
   287
    require(c.debug_index.isDefined)
wenzelm@61010
   288
wenzelm@65213
   289
    state.change(st => {
wenzelm@61014
   290
      input(c.thread_name, "print_vals", c.debug_index.getOrElse(0).toString,
wenzelm@61010
   291
        SML.toString, Symbol.encode(context))
wenzelm@65213
   292
      st.clear_output(c.thread_name)
wenzelm@60897
   293
    })
wenzelm@60902
   294
    delay_update.invoke()
wenzelm@60897
   295
  }
wenzelm@60749
   296
}