# HG changeset patch
# User wenzelm
# Date 1439318962 -7200
# Node ID ce8abd005c5deacae0af92746c06bf7802607f39
# Parent  11a0f333de6f0d6b120cf647790999b62355af03
clarified GUI event handling;

diff -r 11a0f333de6f -r ce8abd005c5d src/Pure/Tools/debugger.scala
--- 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 => {
diff -r 11a0f333de6f -r ce8abd005c5d src/Tools/jEdit/src/debugger_dockable.scala
--- 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