src/Tools/jEdit/src/debugger_dockable.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:      Tools/jEdit/src/debugger_dockable.scala
wenzelm@60749
     2
    Author:     Makarius
wenzelm@60749
     3
wenzelm@60749
     4
Dockable window for Isabelle/ML debugger.
wenzelm@60749
     5
*/
wenzelm@60749
     6
wenzelm@60749
     7
package isabelle.jedit
wenzelm@60749
     8
wenzelm@60749
     9
wenzelm@60749
    10
import isabelle._
wenzelm@60749
    11
wenzelm@60848
    12
import java.awt.{BorderLayout, Dimension}
wenzelm@60875
    13
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, MouseEvent, MouseAdapter,
wenzelm@60875
    14
  FocusAdapter, FocusEvent}
wenzelm@60848
    15
import javax.swing.{JTree, JScrollPane}
wenzelm@60850
    16
import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
wenzelm@60848
    17
import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
wenzelm@60832
    18
wenzelm@60857
    19
import scala.swing.{Button, Label, Component, SplitPane, Orientation, CheckBox}
wenzelm@60832
    20
import scala.swing.event.ButtonClicked
wenzelm@60749
    21
wenzelm@60875
    22
import org.gjt.sp.jedit.{jEdit, View}
wenzelm@60749
    23
wenzelm@60749
    24
wenzelm@60848
    25
object Debugger_Dockable
wenzelm@60848
    26
{
wenzelm@60851
    27
  sealed case class Thread_Entry(thread_name: String, debug_states: List[Debugger.Debug_State])
wenzelm@60848
    28
  {
wenzelm@60848
    29
    override def toString: String = thread_name
wenzelm@60848
    30
  }
wenzelm@60851
    31
wenzelm@60851
    32
  sealed case class Stack_Entry(debug_state: Debugger.Debug_State, index: Int)
wenzelm@60851
    33
  {
wenzelm@60851
    34
    override def toString: String = debug_state.function
wenzelm@60851
    35
  }
wenzelm@60848
    36
}
wenzelm@60848
    37
wenzelm@60749
    38
class Debugger_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@60749
    39
{
wenzelm@60749
    40
  GUI_Thread.require {}
wenzelm@60749
    41
wenzelm@60749
    42
wenzelm@60749
    43
  /* component state -- owned by GUI thread */
wenzelm@60749
    44
wenzelm@60749
    45
  private var current_snapshot = Document.Snapshot.init
wenzelm@60848
    46
  private var current_threads: Map[String, List[Debugger.Debug_State]] = Map.empty
wenzelm@60749
    47
  private var current_output: List[XML.Tree] = Nil
wenzelm@60749
    48
wenzelm@60749
    49
wenzelm@60848
    50
  /* pretty text area */
wenzelm@60848
    51
wenzelm@60848
    52
  val pretty_text_area = new Pretty_Text_Area(view)
wenzelm@60848
    53
wenzelm@60848
    54
  override def detach_operation = pretty_text_area.detach_operation
wenzelm@60848
    55
wenzelm@60848
    56
  private def handle_resize()
wenzelm@60848
    57
  {
wenzelm@60848
    58
    GUI_Thread.require {}
wenzelm@60848
    59
wenzelm@60848
    60
    pretty_text_area.resize(
wenzelm@60848
    61
      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
wenzelm@60848
    62
  }
wenzelm@60848
    63
wenzelm@60848
    64
  private def handle_update()
wenzelm@60848
    65
  {
wenzelm@60848
    66
    GUI_Thread.require {}
wenzelm@60848
    67
wenzelm@60848
    68
    val new_state = Debugger.current_state()
wenzelm@60848
    69
wenzelm@60848
    70
    val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
wenzelm@60848
    71
    val new_threads = new_state.threads
wenzelm@60851
    72
    val new_output =
wenzelm@60851
    73
    {
wenzelm@60859
    74
      val current_thread_selection = thread_selection()
wenzelm@60851
    75
      (for {
wenzelm@60851
    76
        (thread_name, results) <- new_state.output
wenzelm@60859
    77
        if current_thread_selection.isEmpty || current_thread_selection.get == thread_name
wenzelm@60851
    78
        (_, tree) <- results.iterator
wenzelm@60851
    79
      } yield tree).toList
wenzelm@60851
    80
    }
wenzelm@60848
    81
wenzelm@60848
    82
    if (new_threads != current_threads) {
wenzelm@60851
    83
      val thread_entries =
wenzelm@60848
    84
        (for ((a, b) <- new_threads.iterator)
wenzelm@60851
    85
          yield Debugger_Dockable.Thread_Entry(a, b)).toList.sortBy(_.thread_name)
wenzelm@60851
    86
      update_tree(thread_entries)
wenzelm@60848
    87
    }
wenzelm@60848
    88
wenzelm@60848
    89
    if (new_output != current_output)
wenzelm@60848
    90
      pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))
wenzelm@60848
    91
wenzelm@60848
    92
    current_snapshot = new_snapshot
wenzelm@60848
    93
    current_threads = new_threads
wenzelm@60848
    94
    current_output = new_output
wenzelm@60848
    95
  }
wenzelm@60848
    96
wenzelm@60848
    97
wenzelm@60848
    98
  /* tree view */
wenzelm@60848
    99
wenzelm@60848
   100
  private val root = new DefaultMutableTreeNode("Threads")
wenzelm@60848
   101
wenzelm@60848
   102
  val tree = new JTree(root)
wenzelm@60848
   103
  tree.setRowHeight(0)
wenzelm@60848
   104
  tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
wenzelm@60848
   105
wenzelm@60854
   106
  def tree_selection(): Option[(Debugger_Dockable.Thread_Entry, Option[Int])] =
wenzelm@60851
   107
    tree.getSelectionPath match {
wenzelm@60851
   108
      case null => None
wenzelm@60851
   109
      case path =>
wenzelm@60851
   110
        path.getPath.toList.map(n => n.asInstanceOf[DefaultMutableTreeNode].getUserObject) match {
wenzelm@60851
   111
          case List(_, t: Debugger_Dockable.Thread_Entry) =>
wenzelm@60854
   112
            Some((t, None))
wenzelm@60851
   113
          case List(_, t: Debugger_Dockable.Thread_Entry, s: Debugger_Dockable.Stack_Entry) =>
wenzelm@60854
   114
            Some((t, Some(s.index)))
wenzelm@60851
   115
          case _ => None
wenzelm@60851
   116
        }
wenzelm@60851
   117
    }
wenzelm@60851
   118
wenzelm@60859
   119
  def thread_selection(): Option[String] = tree_selection().map(sel => sel._1.thread_name)
wenzelm@60859
   120
wenzelm@60875
   121
  def focus_selection(): Option[Position.T] =
wenzelm@60875
   122
    tree_selection() match {
wenzelm@60875
   123
      case Some((t, opt_index)) =>
wenzelm@60875
   124
        val i = opt_index getOrElse 0
wenzelm@60875
   125
        if (i < t.debug_states.length) Some(t.debug_states(i).pos) else None
wenzelm@60875
   126
      case _ => None
wenzelm@60875
   127
    }
wenzelm@60875
   128
wenzelm@60851
   129
  private def update_tree(thread_entries: List[Debugger_Dockable.Thread_Entry])
wenzelm@60848
   130
  {
wenzelm@60860
   131
    val old_thread_selection = thread_selection()
wenzelm@60860
   132
wenzelm@60848
   133
    tree.clearSelection
wenzelm@60848
   134
    root.removeAllChildren
wenzelm@60848
   135
wenzelm@60859
   136
    for (thread_entry <- thread_entries) {
wenzelm@60859
   137
      val thread_node = new DefaultMutableTreeNode(thread_entry)
wenzelm@60851
   138
      for ((debug_state, i) <- thread_entry.debug_states.zipWithIndex) {
wenzelm@60859
   139
        val stack_node =
wenzelm@60859
   140
          new DefaultMutableTreeNode(Debugger_Dockable.Stack_Entry(debug_state, i))
wenzelm@60859
   141
        thread_node.add(stack_node)
wenzelm@60848
   142
      }
wenzelm@60859
   143
      root.add(thread_node)
wenzelm@60848
   144
    }
wenzelm@60848
   145
wenzelm@60859
   146
    tree.getModel.asInstanceOf[DefaultTreeModel].reload(root)
wenzelm@60860
   147
wenzelm@60860
   148
    old_thread_selection match {
wenzelm@60860
   149
      case Some(thread_name) if thread_entries.exists(t => t.thread_name == thread_name) =>
wenzelm@60860
   150
        val i =
wenzelm@60860
   151
          (for (t <- thread_entries.iterator.takeWhile(t => t.thread_name != thread_name))
wenzelm@60860
   152
            yield 1 + t.debug_states.length).sum
wenzelm@60860
   153
        tree.addSelectionRow(i + 1)
wenzelm@60860
   154
      case _ =>
wenzelm@60860
   155
    }
wenzelm@60859
   156
    for (i <- 0 until tree.getRowCount) tree.expandRow(i)
wenzelm@60860
   157
wenzelm@60848
   158
    tree.revalidate()
wenzelm@60848
   159
  }
wenzelm@60848
   160
wenzelm@60875
   161
  tree.addTreeSelectionListener(
wenzelm@60875
   162
    new TreeSelectionListener {
wenzelm@60875
   163
      override def valueChanged(e: TreeSelectionEvent) { update_focus(focus_selection()) }
wenzelm@60875
   164
    })
wenzelm@60848
   165
wenzelm@60848
   166
  tree.addMouseListener(new MouseAdapter {
wenzelm@60848
   167
    override def mouseClicked(e: MouseEvent)
wenzelm@60848
   168
    {
wenzelm@60848
   169
      val click = tree.getPathForLocation(e.getX, e.getY)
wenzelm@60848
   170
      if (click != null && e.getClickCount == 1) {
wenzelm@60848
   171
        (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
wenzelm@60848
   172
          case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
wenzelm@60875
   173
            handle_update()
wenzelm@60848
   174
          case _ =>
wenzelm@60848
   175
        }
wenzelm@60848
   176
      }
wenzelm@60848
   177
    }
wenzelm@60848
   178
  })
wenzelm@60848
   179
wenzelm@60848
   180
  val tree_view = new JScrollPane(tree)
wenzelm@60849
   181
  tree_view.setMinimumSize(new Dimension(200, 50))
wenzelm@60848
   182
wenzelm@60848
   183
wenzelm@60848
   184
  /* controls */
wenzelm@60832
   185
wenzelm@60862
   186
  private val context_label = new Label("Context:") {
wenzelm@60862
   187
    tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic"
wenzelm@60862
   188
  }
wenzelm@60832
   189
  private val context_field =
wenzelm@60832
   190
    new Completion_Popup.History_Text_Field("isabelle-debugger-context")
wenzelm@60832
   191
    {
wenzelm@60832
   192
      setColumns(20)
wenzelm@60832
   193
      setToolTipText(context_label.tooltip)
wenzelm@60832
   194
      setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
wenzelm@60832
   195
    }
wenzelm@60832
   196
wenzelm@60862
   197
  private val expression_label = new Label("ML:") {
wenzelm@60862
   198
    tooltip = "Isabelle/ML or Standard ML expression"
wenzelm@60862
   199
  }
wenzelm@60832
   200
  private val expression_field =
wenzelm@60832
   201
    new Completion_Popup.History_Text_Field("isabelle-debugger-expression")
wenzelm@60832
   202
    {
wenzelm@60832
   203
      override def processKeyEvent(evt: KeyEvent)
wenzelm@60832
   204
      {
wenzelm@60832
   205
        if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
wenzelm@60832
   206
          eval_expression()
wenzelm@60832
   207
        super.processKeyEvent(evt)
wenzelm@60832
   208
      }
wenzelm@60832
   209
      { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
wenzelm@60832
   210
      setColumns(40)
wenzelm@60832
   211
      setToolTipText(expression_label.tooltip)
wenzelm@60832
   212
      setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
wenzelm@60832
   213
    }
wenzelm@60832
   214
wenzelm@60857
   215
  private val sml_button = new CheckBox("SML") {
wenzelm@60857
   216
    tooltip = "Official Standard ML instead of Isabelle/ML"
wenzelm@60857
   217
    selected = false
wenzelm@60857
   218
  }
wenzelm@60857
   219
wenzelm@60832
   220
  private val eval_button = new Button("<html><b>Eval</b></html>") {
wenzelm@60862
   221
      tooltip = "Evaluate ML expression within optional context"
wenzelm@60832
   222
      reactions += { case ButtonClicked(_) => eval_expression() }
wenzelm@60832
   223
    }
wenzelm@60832
   224
wenzelm@60832
   225
  private def eval_expression()
wenzelm@60832
   226
  {
wenzelm@60861
   227
    context_field.addCurrentToHistory()
wenzelm@60861
   228
    expression_field.addCurrentToHistory()
wenzelm@60856
   229
    tree_selection() match {
wenzelm@60857
   230
      case Some((t, opt_index)) if t.debug_states.nonEmpty =>
wenzelm@60857
   231
        Debugger.eval(t.thread_name, opt_index getOrElse 0,
wenzelm@60857
   232
          sml_button.selected, context_field.getText, expression_field.getText)
wenzelm@60856
   233
      case _ =>
wenzelm@60856
   234
    }
wenzelm@60832
   235
  }
wenzelm@60832
   236
wenzelm@60869
   237
  private val step_button = new Button("Step") {
wenzelm@60869
   238
    tooltip = "Single-step in depth-first order"
wenzelm@60869
   239
    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step(_)) }
wenzelm@60869
   240
  }
wenzelm@60869
   241
wenzelm@60869
   242
  private val step_over_button = new Button("Step over") {
wenzelm@60869
   243
    tooltip = "Single-step within this function"
wenzelm@60869
   244
    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step_over(_)) }
wenzelm@60869
   245
  }
wenzelm@60869
   246
wenzelm@60869
   247
  private val step_out_button = new Button("Step out") {
wenzelm@60869
   248
    tooltip = "Single-step outside this function"
wenzelm@60869
   249
    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step_out(_)) }
wenzelm@60869
   250
  }
wenzelm@60869
   251
wenzelm@60854
   252
  private val continue_button = new Button("Continue") {
wenzelm@60869
   253
    tooltip = "Continue program on current thread, until next breakpoint"
wenzelm@60869
   254
    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.continue(_)) }
wenzelm@60869
   255
  }
wenzelm@60854
   256
wenzelm@60854
   257
  private val cancel_button = new Button("Cancel") {
wenzelm@60869
   258
    tooltip = "Interrupt program on current thread"
wenzelm@60869
   259
    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.cancel(_)) }
wenzelm@60869
   260
  }
wenzelm@60854
   261
wenzelm@60845
   262
  private val debugger_active =
wenzelm@60845
   263
    new JEdit_Options.Check_Box("ML_debugger_active", "Active", "Enable debugger at run-time")
wenzelm@60845
   264
wenzelm@60845
   265
  private val debugger_stepping =
wenzelm@60845
   266
    new JEdit_Options.Check_Box("ML_debugger_stepping", "Stepping", "Enable single-step mode")
wenzelm@60845
   267
wenzelm@60832
   268
  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
wenzelm@60832
   269
wenzelm@60848
   270
  private val controls =
wenzelm@60848
   271
    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
wenzelm@60869
   272
      step_button, step_over_button, step_out_button, continue_button, cancel_button,
wenzelm@60848
   273
      context_label, Component.wrap(context_field),
wenzelm@60857
   274
      expression_label, Component.wrap(expression_field),
wenzelm@60869
   275
      sml_button, eval_button,
wenzelm@60848
   276
      pretty_text_area.search_label, pretty_text_area.search_field,
wenzelm@60848
   277
      debugger_stepping, debugger_active, zoom)
wenzelm@60848
   278
  add(controls.peer, BorderLayout.NORTH)
wenzelm@60749
   279
wenzelm@60749
   280
wenzelm@60875
   281
  /* focus */
wenzelm@60875
   282
wenzelm@60875
   283
  override def focusOnDefaultComponent { eval_button.requestFocus }
wenzelm@60875
   284
wenzelm@60875
   285
  addFocusListener(new FocusAdapter {
wenzelm@60875
   286
    override def focusGained(e: FocusEvent) { update_focus(focus_selection()) }
wenzelm@60875
   287
    override def focusLost(e: FocusEvent) { update_focus(None) }
wenzelm@60875
   288
  })
wenzelm@60875
   289
wenzelm@60875
   290
  private def update_focus(focus: Option[Position.T])
wenzelm@60875
   291
  {
wenzelm@60875
   292
    if (Debugger.focus(focus) && focus.isDefined)
wenzelm@60875
   293
      PIDE.editor.hyperlink_position(current_snapshot, focus.get).foreach(_.follow(view))
wenzelm@60875
   294
  }
wenzelm@60875
   295
wenzelm@60875
   296
wenzelm@60848
   297
  /* main panel */
wenzelm@60749
   298
wenzelm@60848
   299
  val main_panel = new SplitPane(Orientation.Vertical) {
wenzelm@60848
   300
    oneTouchExpandable = true
wenzelm@60848
   301
    leftComponent = Component.wrap(tree_view)
wenzelm@60848
   302
    rightComponent = Component.wrap(pretty_text_area)
wenzelm@60749
   303
  }
wenzelm@60848
   304
  set_content(main_panel)
wenzelm@60749
   305
wenzelm@60749
   306
wenzelm@60749
   307
  /* main */
wenzelm@60749
   308
wenzelm@60749
   309
  private val main =
wenzelm@60749
   310
    Session.Consumer[Any](getClass.getName) {
wenzelm@60749
   311
      case _: Session.Global_Options =>
wenzelm@60835
   312
        Debugger.init(PIDE.session)
wenzelm@60845
   313
        GUI_Thread.later {
wenzelm@60845
   314
          debugger_active.load()
wenzelm@60845
   315
          debugger_stepping.load()
wenzelm@60845
   316
          handle_resize()
wenzelm@60845
   317
        }
wenzelm@60749
   318
wenzelm@60835
   319
      case _: Debugger.Update =>
wenzelm@60749
   320
        GUI_Thread.later { handle_update() }
wenzelm@60749
   321
    }
wenzelm@60749
   322
wenzelm@60749
   323
  override def init()
wenzelm@60749
   324
  {
wenzelm@60749
   325
    PIDE.session.global_options += main
wenzelm@60835
   326
    PIDE.session.debugger_updates += main
wenzelm@60835
   327
    Debugger.init(PIDE.session)
wenzelm@60876
   328
    Debugger.inc_active()
wenzelm@60749
   329
    handle_update()
wenzelm@60876
   330
    jEdit.propertiesChanged()
wenzelm@60749
   331
  }
wenzelm@60749
   332
wenzelm@60749
   333
  override def exit()
wenzelm@60749
   334
  {
wenzelm@60749
   335
    PIDE.session.global_options -= main
wenzelm@60835
   336
    PIDE.session.debugger_updates -= main
wenzelm@60749
   337
    delay_resize.revoke()
wenzelm@60875
   338
    update_focus(None)
wenzelm@60876
   339
    Debugger.dec_active()
wenzelm@60876
   340
    jEdit.propertiesChanged()
wenzelm@60749
   341
  }
wenzelm@60749
   342
wenzelm@60749
   343
wenzelm@60749
   344
  /* resize */
wenzelm@60749
   345
wenzelm@60749
   346
  private val delay_resize =
wenzelm@60749
   347
    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm@60749
   348
wenzelm@60749
   349
  addComponentListener(new ComponentAdapter {
wenzelm@60749
   350
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@60750
   351
    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@60749
   352
  })
wenzelm@60749
   353
}