src/Tools/jEdit/src/debugger_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 61018 32cc7d219c38
child 64882 c3b42ac0cf81
permissions -rw-r--r--
tuned signature;
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@61007
    13
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, FocusAdapter, FocusEvent,
wenzelm@61007
    14
  MouseEvent, MouseAdapter}
wenzelm@60883
    15
import javax.swing.{JTree, JMenuItem}
wenzelm@60850
    16
import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
wenzelm@60848
    17
import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
wenzelm@60832
    18
wenzelm@61016
    19
import scala.collection.immutable.SortedMap
wenzelm@60883
    20
import scala.swing.{Button, Label, Component, ScrollPane, SplitPane, Orientation,
wenzelm@60883
    21
  CheckBox, BorderPanel}
wenzelm@60832
    22
import scala.swing.event.ButtonClicked
wenzelm@60749
    23
wenzelm@60875
    24
import org.gjt.sp.jedit.{jEdit, View}
wenzelm@60878
    25
import org.gjt.sp.jedit.menu.EnhancedMenuItem
wenzelm@60878
    26
import org.gjt.sp.jedit.textarea.JEditTextArea
wenzelm@60749
    27
wenzelm@60749
    28
wenzelm@60848
    29
object Debugger_Dockable
wenzelm@60848
    30
{
wenzelm@60878
    31
  /* breakpoints */
wenzelm@60878
    32
wenzelm@60880
    33
  def toggle_breakpoint(command: Command, breakpoint: Long)
wenzelm@60878
    34
  {
wenzelm@60878
    35
    GUI_Thread.require {}
wenzelm@60878
    36
wenzelm@60880
    37
    Debugger.toggle_breakpoint(command, breakpoint)
wenzelm@60878
    38
    jEdit.propertiesChanged()
wenzelm@60878
    39
  }
wenzelm@60878
    40
wenzelm@60880
    41
  def get_breakpoint(text_area: JEditTextArea, offset: Text.Offset): Option[(Command, Long)] =
wenzelm@60878
    42
  {
wenzelm@60878
    43
    GUI_Thread.require {}
wenzelm@60878
    44
wenzelm@60878
    45
    PIDE.document_view(text_area) match {
wenzelm@60878
    46
      case Some(doc_view) =>
wenzelm@60878
    47
        val rendering = doc_view.get_rendering()
wenzelm@60878
    48
        val range = JEdit_Lib.point_range(text_area.getBuffer, offset)
wenzelm@60880
    49
        rendering.breakpoint(range)
wenzelm@60878
    50
      case None => None
wenzelm@60878
    51
    }
wenzelm@60878
    52
  }
wenzelm@60878
    53
wenzelm@60878
    54
wenzelm@60878
    55
  /* context menu */
wenzelm@60878
    56
wenzelm@60878
    57
  def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] =
wenzelm@60890
    58
    if (Debugger.is_active() && get_breakpoint(text_area, offset).isDefined) {
wenzelm@60878
    59
      val context = jEdit.getActionContext()
wenzelm@60878
    60
      val name = "isabelle.toggle-breakpoint"
wenzelm@60878
    61
      List(new EnhancedMenuItem(context.getAction(name).getLabel, name, context))
wenzelm@60878
    62
    }
wenzelm@60878
    63
    else Nil
wenzelm@60848
    64
}
wenzelm@60848
    65
wenzelm@60749
    66
class Debugger_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@60749
    67
{
wenzelm@60749
    68
  GUI_Thread.require {}
wenzelm@60749
    69
wenzelm@60749
    70
wenzelm@60749
    71
  /* component state -- owned by GUI thread */
wenzelm@60749
    72
wenzelm@60749
    73
  private var current_snapshot = Document.Snapshot.init
wenzelm@61016
    74
  private var current_threads: Debugger.Threads = SortedMap.empty
wenzelm@60749
    75
  private var current_output: List[XML.Tree] = Nil
wenzelm@60749
    76
wenzelm@60749
    77
wenzelm@60848
    78
  /* pretty text area */
wenzelm@60848
    79
wenzelm@60848
    80
  val pretty_text_area = new Pretty_Text_Area(view)
wenzelm@60848
    81
wenzelm@60848
    82
  override def detach_operation = pretty_text_area.detach_operation
wenzelm@60848
    83
wenzelm@60848
    84
  private def handle_resize()
wenzelm@60848
    85
  {
wenzelm@60848
    86
    GUI_Thread.require {}
wenzelm@60848
    87
wenzelm@60848
    88
    pretty_text_area.resize(
wenzelm@60848
    89
      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
wenzelm@60848
    90
  }
wenzelm@60848
    91
wenzelm@60848
    92
  private def handle_update()
wenzelm@60848
    93
  {
wenzelm@60848
    94
    GUI_Thread.require {}
wenzelm@60848
    95
wenzelm@60848
    96
    val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
wenzelm@61018
    97
    val (new_threads, new_output) = Debugger.status(tree_selection())
wenzelm@60848
    98
wenzelm@61018
    99
    if (new_threads != current_threads)
wenzelm@61018
   100
      update_tree(new_threads)
wenzelm@60848
   101
wenzelm@60848
   102
    if (new_output != current_output)
wenzelm@60848
   103
      pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))
wenzelm@60848
   104
wenzelm@60848
   105
    current_snapshot = new_snapshot
wenzelm@60848
   106
    current_threads = new_threads
wenzelm@60848
   107
    current_output = new_output
wenzelm@60848
   108
  }
wenzelm@60848
   109
wenzelm@60848
   110
wenzelm@60848
   111
  /* tree view */
wenzelm@60848
   112
wenzelm@60848
   113
  private val root = new DefaultMutableTreeNode("Threads")
wenzelm@60848
   114
wenzelm@60848
   115
  val tree = new JTree(root)
wenzelm@60848
   116
  tree.setRowHeight(0)
wenzelm@60848
   117
  tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
wenzelm@60848
   118
wenzelm@61010
   119
  def tree_selection(): Option[Debugger.Context] =
wenzelm@61010
   120
    tree.getLastSelectedPathComponent match {
wenzelm@61010
   121
      case node: DefaultMutableTreeNode =>
wenzelm@61010
   122
        node.getUserObject match {
wenzelm@61010
   123
          case c: Debugger.Context => Some(c)
wenzelm@60851
   124
          case _ => None
wenzelm@60851
   125
        }
wenzelm@60875
   126
      case _ => None
wenzelm@60875
   127
    }
wenzelm@60875
   128
wenzelm@61010
   129
  def thread_selection(): Option[String] = tree_selection().map(_.thread_name)
wenzelm@61010
   130
wenzelm@61018
   131
  private def update_tree(threads: Debugger.Threads)
wenzelm@60848
   132
  {
wenzelm@61018
   133
    val thread_contexts =
wenzelm@61018
   134
      (for ((a, b) <- threads.iterator)
wenzelm@61018
   135
        yield Debugger.Context(a, b)).toList
wenzelm@61010
   136
wenzelm@61010
   137
    val new_tree_selection =
wenzelm@61009
   138
      tree_selection() match {
wenzelm@61018
   139
        case Some(c) if thread_contexts.contains(c) => Some(c)
wenzelm@61018
   140
        case Some(c) if thread_contexts.exists(t => c.thread_name == t.thread_name) =>
wenzelm@61018
   141
          Some(c.reset)
wenzelm@61018
   142
        case _ => thread_contexts.headOption
wenzelm@60906
   143
      }
wenzelm@60860
   144
wenzelm@60848
   145
    tree.clearSelection
wenzelm@60848
   146
    root.removeAllChildren
wenzelm@60848
   147
wenzelm@61018
   148
    for (thread <- thread_contexts) {
wenzelm@61010
   149
      val thread_node = new DefaultMutableTreeNode(thread)
wenzelm@61010
   150
      for ((debug_state, i) <- thread.debug_states.zipWithIndex)
wenzelm@61010
   151
        thread_node.add(new DefaultMutableTreeNode(thread.select(i)))
wenzelm@60859
   152
      root.add(thread_node)
wenzelm@60848
   153
    }
wenzelm@60848
   154
wenzelm@60859
   155
    tree.getModel.asInstanceOf[DefaultTreeModel].reload(root)
wenzelm@60860
   156
wenzelm@60905
   157
    tree.expandRow(0)
wenzelm@60905
   158
    for (i <- Range.inclusive(tree.getRowCount - 1, 1, -1)) tree.expandRow(i)
wenzelm@60905
   159
wenzelm@61009
   160
    new_tree_selection match {
wenzelm@61010
   161
      case Some(c) =>
wenzelm@60860
   162
        val i =
wenzelm@61018
   163
          (for (t <- thread_contexts.iterator.takeWhile(t => c.thread_name != t.thread_name))
wenzelm@61010
   164
            yield t.size).sum
wenzelm@61010
   165
        tree.addSelectionRow(i + c.index + 1)
wenzelm@60906
   166
      case None =>
wenzelm@60860
   167
    }
wenzelm@60860
   168
wenzelm@60848
   169
    tree.revalidate()
wenzelm@60848
   170
  }
wenzelm@60848
   171
wenzelm@60901
   172
  def update_vals()
wenzelm@60901
   173
  {
wenzelm@60901
   174
    tree_selection() match {
wenzelm@61010
   175
      case Some(c) if c.stack_state.isDefined =>
wenzelm@61010
   176
        Debugger.print_vals(c, sml_button.selected, context_field.getText)
wenzelm@61010
   177
      case Some(c) =>
wenzelm@61010
   178
        Debugger.clear_output(c.thread_name)
wenzelm@61010
   179
      case None =>
wenzelm@60901
   180
    }
wenzelm@60901
   181
  }
wenzelm@60901
   182
wenzelm@60875
   183
  tree.addTreeSelectionListener(
wenzelm@60875
   184
    new TreeSelectionListener {
wenzelm@60901
   185
      override def valueChanged(e: TreeSelectionEvent) {
wenzelm@61014
   186
        update_focus()
wenzelm@60901
   187
        update_vals()
wenzelm@60901
   188
      }
wenzelm@60875
   189
    })
wenzelm@61007
   190
  tree.addMouseListener(
wenzelm@61007
   191
    new MouseAdapter {
wenzelm@61007
   192
      override def mouseClicked(e: MouseEvent)
wenzelm@61007
   193
      {
wenzelm@61007
   194
        val click = tree.getPathForLocation(e.getX, e.getY)
wenzelm@61007
   195
        if (click != null && e.getClickCount == 1)
wenzelm@61014
   196
          update_focus()
wenzelm@61007
   197
      }
wenzelm@61007
   198
    })
wenzelm@60848
   199
wenzelm@60883
   200
  private val tree_pane = new ScrollPane(Component.wrap(tree))
wenzelm@60883
   201
  tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
wenzelm@60883
   202
  tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
wenzelm@60883
   203
  tree_pane.minimumSize = new Dimension(200, 100)
wenzelm@60848
   204
wenzelm@60848
   205
wenzelm@60848
   206
  /* controls */
wenzelm@60832
   207
wenzelm@60932
   208
  private val break_button = new CheckBox("Break") {
wenzelm@60932
   209
    tooltip = "Break running threads at next possible breakpoint"
wenzelm@60932
   210
    selected = Debugger.is_break()
wenzelm@60932
   211
    reactions += { case ButtonClicked(_) => Debugger.set_break(selected) }
wenzelm@60932
   212
  }
wenzelm@60932
   213
wenzelm@60907
   214
  private val continue_button = new Button("Continue") {
wenzelm@60907
   215
    tooltip = "Continue program on current thread, until next breakpoint"
wenzelm@60907
   216
    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.continue(_)) }
wenzelm@60907
   217
  }
wenzelm@60907
   218
wenzelm@60907
   219
  private val step_button = new Button("Step") {
wenzelm@60907
   220
    tooltip = "Single-step in depth-first order"
wenzelm@60907
   221
    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step(_)) }
wenzelm@60907
   222
  }
wenzelm@60907
   223
wenzelm@60907
   224
  private val step_over_button = new Button("Step over") {
wenzelm@60907
   225
    tooltip = "Single-step within this function"
wenzelm@60907
   226
    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step_over(_)) }
wenzelm@60907
   227
  }
wenzelm@60907
   228
wenzelm@60907
   229
  private val step_out_button = new Button("Step out") {
wenzelm@60907
   230
    tooltip = "Single-step outside this function"
wenzelm@60907
   231
    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step_out(_)) }
wenzelm@60907
   232
  }
wenzelm@60907
   233
wenzelm@60862
   234
  private val context_label = new Label("Context:") {
wenzelm@60862
   235
    tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic"
wenzelm@60862
   236
  }
wenzelm@60832
   237
  private val context_field =
wenzelm@60832
   238
    new Completion_Popup.History_Text_Field("isabelle-debugger-context")
wenzelm@60832
   239
    {
wenzelm@60936
   240
      override def processKeyEvent(evt: KeyEvent)
wenzelm@60936
   241
      {
wenzelm@60936
   242
        if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
wenzelm@60936
   243
          eval_expression()
wenzelm@60936
   244
        super.processKeyEvent(evt)
wenzelm@60936
   245
      }
wenzelm@60832
   246
      setColumns(20)
wenzelm@60832
   247
      setToolTipText(context_label.tooltip)
wenzelm@60832
   248
      setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
wenzelm@60832
   249
    }
wenzelm@60832
   250
wenzelm@60862
   251
  private val expression_label = new Label("ML:") {
wenzelm@60862
   252
    tooltip = "Isabelle/ML or Standard ML expression"
wenzelm@60862
   253
  }
wenzelm@60832
   254
  private val expression_field =
wenzelm@60832
   255
    new Completion_Popup.History_Text_Field("isabelle-debugger-expression")
wenzelm@60832
   256
    {
wenzelm@60832
   257
      override def processKeyEvent(evt: KeyEvent)
wenzelm@60832
   258
      {
wenzelm@60832
   259
        if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
wenzelm@60832
   260
          eval_expression()
wenzelm@60832
   261
        super.processKeyEvent(evt)
wenzelm@60832
   262
      }
wenzelm@60832
   263
      { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
wenzelm@60832
   264
      setColumns(40)
wenzelm@60832
   265
      setToolTipText(expression_label.tooltip)
wenzelm@60832
   266
      setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
wenzelm@60832
   267
    }
wenzelm@60832
   268
wenzelm@60832
   269
  private val eval_button = new Button("<html><b>Eval</b></html>") {
wenzelm@60862
   270
      tooltip = "Evaluate ML expression within optional context"
wenzelm@60832
   271
      reactions += { case ButtonClicked(_) => eval_expression() }
wenzelm@60832
   272
    }
wenzelm@60832
   273
wenzelm@60832
   274
  private def eval_expression()
wenzelm@60832
   275
  {
wenzelm@60861
   276
    context_field.addCurrentToHistory()
wenzelm@60861
   277
    expression_field.addCurrentToHistory()
wenzelm@60856
   278
    tree_selection() match {
wenzelm@61014
   279
      case Some(c) if c.debug_index.isDefined =>
wenzelm@61010
   280
        Debugger.eval(c, sml_button.selected, context_field.getText, expression_field.getText)
wenzelm@60856
   281
      case _ =>
wenzelm@60856
   282
    }
wenzelm@60832
   283
  }
wenzelm@60832
   284
wenzelm@60907
   285
  private val sml_button = new CheckBox("SML") {
wenzelm@60907
   286
    tooltip = "Official Standard ML instead of Isabelle/ML"
wenzelm@60907
   287
    selected = false
wenzelm@60869
   288
  }
wenzelm@60869
   289
wenzelm@60832
   290
  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
wenzelm@60832
   291
wenzelm@60848
   292
  private val controls =
wenzelm@60848
   293
    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
wenzelm@60932
   294
      break_button, continue_button, step_button, step_over_button, step_out_button,
wenzelm@60848
   295
      context_label, Component.wrap(context_field),
wenzelm@60907
   296
      expression_label, Component.wrap(expression_field), eval_button, sml_button,
wenzelm@60889
   297
      pretty_text_area.search_label, pretty_text_area.search_field, zoom)
wenzelm@60848
   298
  add(controls.peer, BorderLayout.NORTH)
wenzelm@60749
   299
wenzelm@60749
   300
wenzelm@60875
   301
  /* focus */
wenzelm@60875
   302
wenzelm@60875
   303
  override def focusOnDefaultComponent { eval_button.requestFocus }
wenzelm@60875
   304
wenzelm@60875
   305
  addFocusListener(new FocusAdapter {
wenzelm@61014
   306
    override def focusGained(e: FocusEvent) { update_focus() }
wenzelm@60875
   307
  })
wenzelm@60875
   308
wenzelm@61014
   309
  private def update_focus()
wenzelm@60875
   310
  {
wenzelm@61014
   311
    for (c <- tree_selection()) {
wenzelm@61014
   312
      Debugger.set_focus(c)
wenzelm@61014
   313
      for {
wenzelm@61014
   314
        pos <- c.debug_position
wenzelm@61014
   315
        link <- PIDE.editor.hyperlink_position(false, current_snapshot, pos)
wenzelm@61015
   316
      } link.follow(view)
wenzelm@61014
   317
    }
wenzelm@61015
   318
    JEdit_Lib.jedit_text_areas(view.getBuffer).foreach(_.repaint())
wenzelm@60875
   319
  }
wenzelm@60875
   320
wenzelm@60875
   321
wenzelm@60848
   322
  /* main panel */
wenzelm@60749
   323
wenzelm@60848
   324
  val main_panel = new SplitPane(Orientation.Vertical) {
wenzelm@60848
   325
    oneTouchExpandable = true
wenzelm@60883
   326
    leftComponent = tree_pane
wenzelm@60848
   327
    rightComponent = Component.wrap(pretty_text_area)
wenzelm@60749
   328
  }
wenzelm@60848
   329
  set_content(main_panel)
wenzelm@60749
   330
wenzelm@60749
   331
wenzelm@60749
   332
  /* main */
wenzelm@60749
   333
wenzelm@60749
   334
  private val main =
wenzelm@60749
   335
    Session.Consumer[Any](getClass.getName) {
wenzelm@60749
   336
      case _: Session.Global_Options =>
wenzelm@60889
   337
        GUI_Thread.later { handle_resize() }
wenzelm@60749
   338
wenzelm@60900
   339
      case Debugger.Update =>
wenzelm@60932
   340
        GUI_Thread.later {
wenzelm@60932
   341
          break_button.selected = Debugger.is_break()
wenzelm@60932
   342
          handle_update()
wenzelm@60932
   343
        }
wenzelm@60749
   344
    }
wenzelm@60749
   345
wenzelm@60749
   346
  override def init()
wenzelm@60749
   347
  {
wenzelm@60749
   348
    PIDE.session.global_options += main
wenzelm@60835
   349
    PIDE.session.debugger_updates += main
wenzelm@60910
   350
    Debugger.init()
wenzelm@60749
   351
    handle_update()
wenzelm@60876
   352
    jEdit.propertiesChanged()
wenzelm@60749
   353
  }
wenzelm@60749
   354
wenzelm@60749
   355
  override def exit()
wenzelm@60749
   356
  {
wenzelm@60749
   357
    PIDE.session.global_options -= main
wenzelm@60835
   358
    PIDE.session.debugger_updates -= main
wenzelm@60749
   359
    delay_resize.revoke()
wenzelm@60910
   360
    Debugger.exit()
wenzelm@60876
   361
    jEdit.propertiesChanged()
wenzelm@60749
   362
  }
wenzelm@60749
   363
wenzelm@60749
   364
wenzelm@60749
   365
  /* resize */
wenzelm@60749
   366
wenzelm@60749
   367
  private val delay_resize =
wenzelm@60749
   368
    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm@60749
   369
wenzelm@60749
   370
  addComponentListener(new ComponentAdapter {
wenzelm@60749
   371
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@60750
   372
    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@60749
   373
  })
wenzelm@60749
   374
}