--- a/src/Pure/Tools/debugger.scala Tue Aug 11 20:32:56 2015 +0200
+++ b/src/Pure/Tools/debugger.scala Tue Aug 11 20:49:22 2015 +0200
@@ -186,6 +186,11 @@
def step_over(thread_name: String): Unit = input(thread_name, "step_over")
def step_out(thread_name: String): Unit = input(thread_name, "step_out")
+ def clear_output(thread_name: String)
+ {
+ global_state.change(_.clear_output(thread_name))
+ }
+
def eval(thread_name: String, index: Int, SML: Boolean, context: String, expression: String)
{
global_state.change(state => {
--- a/src/Tools/jEdit/src/debugger_dockable.scala Tue Aug 11 20:32:56 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Tue Aug 11 20:49:22 2015 +0200
@@ -10,8 +10,7 @@
import isabelle._
import java.awt.{BorderLayout, Dimension}
-import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, MouseEvent, MouseAdapter,
- FocusAdapter, FocusEvent}
+import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, FocusAdapter, FocusEvent}
import javax.swing.{JTree, JMenuItem}
import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
@@ -157,20 +156,14 @@
def thread_selection(): Option[String] = tree_selection().map(sel => sel._1.thread_name)
- def index_selection(): Option[(Debugger_Dockable.Thread_Entry, Int)] =
+ def focus_selection(): Option[Position.T] =
tree_selection() match {
case Some((t, opt_index)) =>
val i = opt_index getOrElse 0
- if (i < t.debug_states.length) Some((t, i)) else None
+ if (i < t.debug_states.length) Some(t.debug_states(i).pos) else None
case _ => None
}
- def focus_selection(): Option[Position.T] =
- index_selection() match {
- case Some((t, i)) => Some(t.debug_states(i).pos)
- case None => None
- }
-
private def update_tree(thread_entries: List[Debugger_Dockable.Thread_Entry])
{
val old_thread_selection =
@@ -205,29 +198,25 @@
tree.revalidate()
}
+ def update_vals()
+ {
+ tree_selection() match {
+ case Some((t, None)) =>
+ Debugger.clear_output(t.thread_name)
+ case Some((t, Some(i))) if i < t.debug_states.length =>
+ Debugger.print_vals(t.thread_name, i, sml_button.selected, context_field.getText)
+ case _ =>
+ }
+ }
+
tree.addTreeSelectionListener(
new TreeSelectionListener {
- override def valueChanged(e: TreeSelectionEvent) { update_focus(focus_selection()) }
+ override def valueChanged(e: TreeSelectionEvent) {
+ update_focus(focus_selection())
+ update_vals()
+ }
})
- 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 =>
- index_selection() match {
- case Some((t, i)) =>
- Debugger.print_vals(t.thread_name, i, sml_button.selected, context_field.getText)
- case None =>
- }
- case _ =>
- }
- }
- }
- })
-
private val tree_pane = new ScrollPane(Component.wrap(tree))
tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always