# HG changeset patch
# User wenzelm
# Date 1440324614 -7200
# Node ID eaceb601a8a2bb51c7d5096f31ac265900a46b22
# Parent  3d62df166e06f12dccabbe02a6931371fcbe3db3
update focus more thoroughly;

diff -r 3d62df166e06 -r eaceb601a8a2 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Sat Aug 22 11:32:34 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Sun Aug 23 12:10:14 2015 +0200
@@ -192,8 +192,8 @@
     })
   }
 
-  def focus(new_focus: Option[Position.T]): Boolean =
-    global_state.change_result(state => (state.focus != new_focus, state.set_focus(new_focus)))
+  def set_focus(focus: Option[Position.T]): Unit =
+    global_state.change(_.set_focus(focus))
 
   def threads(): Map[String, List[Debug_State]] = global_state.value.threads
 
diff -r 3d62df166e06 -r eaceb601a8a2 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sat Aug 22 11:32:34 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sun Aug 23 12:10:14 2015 +0200
@@ -10,7 +10,8 @@
 import isabelle._
 
 import java.awt.{BorderLayout, Dimension}
-import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, FocusAdapter, FocusEvent}
+import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, FocusAdapter, FocusEvent,
+  MouseEvent, MouseAdapter}
 import javax.swing.{JTree, JMenuItem}
 import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
@@ -221,6 +222,15 @@
         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)
+          update_focus(focus_selection())
+      }
+    })
 
   private val tree_pane = new ScrollPane(Component.wrap(tree))
   tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
@@ -335,7 +345,8 @@
 
   private def update_focus(focus: Option[Position.T])
   {
-    if (Debugger.focus(focus) && focus.isDefined)
+    Debugger.set_focus(focus)
+    if (focus.isDefined)
       PIDE.editor.hyperlink_position(false, current_snapshot, focus.get).foreach(_.follow(view))
   }