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