# HG changeset patch # User wenzelm # Date 1438797861 -7200 # Node ID 7ec20b1c8dc9aafbaba4e9bd8c6a5ebf647d29ed # Parent 239d7714392b9e321c8bdde0738f925dd47ca437 more GUI components; diff -r 239d7714392b -r 7ec20b1c8dc9 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Wed Aug 05 20:03:22 2015 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Wed Aug 05 20:04:21 2015 +0200 @@ -9,15 +9,26 @@ import isabelle._ -import java.awt.BorderLayout -import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent} +import java.awt.{BorderLayout, Dimension} +import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, MouseEvent, MouseAdapter} +import javax.swing.{JTree, JScrollPane} +import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel} +import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener} -import scala.swing.{Button, Label, Component} +import scala.swing.{Button, Label, Component, SplitPane, Orientation} import scala.swing.event.ButtonClicked import org.gjt.sp.jedit.View +object Debugger_Dockable +{ + sealed case class Tree_Entry(thread_name: String, debug_states: List[Debugger.Debug_State]) + { + override def toString: String = thread_name + } +} + class Debugger_Dockable(view: View, position: String) extends Dockable(view, position) { GUI_Thread.require {} @@ -26,10 +37,109 @@ /* component state -- owned by GUI thread */ private var current_snapshot = Document.Snapshot.init + private var current_threads: Map[String, List[Debugger.Debug_State]] = Map.empty private var current_output: List[XML.Tree] = Nil - /* common GUI components */ + /* pretty text area */ + + val pretty_text_area = new Pretty_Text_Area(view) + + override def detach_operation = pretty_text_area.detach_operation + + private def handle_resize() + { + GUI_Thread.require {} + + pretty_text_area.resize( + Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100)) + } + + private def handle_update() + { + GUI_Thread.require {} + + val new_state = Debugger.current_state() + + val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot) + val new_threads = new_state.threads + val new_output = // FIXME select by thread name + (for ((_, results) <- new_state.output; (_, tree) <- results.iterator) + yield tree).toList ::: List(XML.Text(new_threads.toString)) + + if (new_threads != current_threads) { + val entries = + (for ((a, b) <- new_threads.iterator) + yield Debugger_Dockable.Tree_Entry(a, b)).toList.sortBy(_.thread_name) + update_tree(entries) + } + + if (new_output != current_output) + pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output)) + + current_snapshot = new_snapshot + current_threads = new_threads + current_output = new_output + + revalidate() + repaint() + } + + + /* tree view */ + + private val root = new DefaultMutableTreeNode("Threads") + + val tree = new JTree(root) + tree.setRowHeight(0) + tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION) + + private def update_tree(entries: List[Debugger_Dockable.Tree_Entry]) + { + tree.clearSelection + + root.removeAllChildren + val entry_nodes = entries.map(entry => new DefaultMutableTreeNode(entry)) + for (node <- entry_nodes) root.add(node) + + for (i <- 0 until tree.getRowCount) tree.expandRow(i) + + for ((entry, node) <- entries zip entry_nodes) { + for (debug_state <- entry.debug_states) { + val sub_node = new DefaultMutableTreeNode(debug_state.function) + node.add(sub_node) + } + } + + tree.revalidate() + } + + private def action(node: DefaultMutableTreeNode) + { + node.getUserObject match { + case _ => // FIXME + } + } + + tree.addMouseListener(new MouseAdapter { + override def mouseClicked(e: MouseEvent) + { + val click = tree.getPathForLocation(e.getX, e.getY) + if (click != null && e.getClickCount == 1) { + (click.getLastPathComponent, tree.getLastSelectedPathComponent) match { + case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 => + action(node) + case _ => + } + } + } + }) + + val tree_view = new JScrollPane(tree) + tree_view.setMinimumSize(new Dimension(100, 50)) + + + /* controls */ private val context_label = new Label("Context:") { tooltip = "Isabelle/ML context (optional)" } private val context_field = @@ -60,6 +170,7 @@ tooltip = "Evaluate Isabelle/ML expression within optional context" reactions += { case ButtonClicked(_) => eval_expression() } } + override def focusOnDefaultComponent { eval_button.requestFocus } private def eval_expression() { @@ -68,9 +179,6 @@ quote(expression_field.getText)) } - - /* controls */ - private val debugger_active = new JEdit_Options.Check_Box("ML_debugger_active", "Active", "Enable debugger at run-time") @@ -79,38 +187,23 @@ private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } - - /* pretty text area */ - - val pretty_text_area = new Pretty_Text_Area(view) - set_content(pretty_text_area) - - override def detach_operation = pretty_text_area.detach_operation + private val controls = + new Wrap_Panel(Wrap_Panel.Alignment.Right)( + context_label, Component.wrap(context_field), + expression_label, Component.wrap(expression_field), eval_button, + pretty_text_area.search_label, pretty_text_area.search_field, + debugger_stepping, debugger_active, zoom) + add(controls.peer, BorderLayout.NORTH) - private def handle_resize() - { - GUI_Thread.require {} - - pretty_text_area.resize( - Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100)) - } - - private def handle_update() - { - GUI_Thread.require {} + /* main panel */ - val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot) - val new_output = // FIXME select by thread name - (for ((_, results) <- Debugger.current_state.output; (_, tree) <- results.iterator) - yield tree).toList ::: List(XML.Text(Debugger.current_state.threads.toString)) - - if (new_output != current_output) - pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output)) - - current_snapshot = new_snapshot - current_output = new_output + val main_panel = new SplitPane(Orientation.Vertical) { + oneTouchExpandable = true + leftComponent = Component.wrap(tree_view) + rightComponent = Component.wrap(pretty_text_area) } + set_content(main_panel) /* main */ @@ -154,15 +247,4 @@ override def componentResized(e: ComponentEvent) { delay_resize.invoke() } override def componentShown(e: ComponentEvent) { delay_resize.invoke() } }) - - - /* controls */ - - private val controls = - new Wrap_Panel(Wrap_Panel.Alignment.Right)( - context_label, Component.wrap(context_field), - expression_label, Component.wrap(expression_field), eval_button, - pretty_text_area.search_label, pretty_text_area.search_field, - debugger_stepping, debugger_active, zoom) - add(controls.peer, BorderLayout.NORTH) }