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