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