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