# HG changeset patch
# User wenzelm
# Date 1439208889 -7200
# Node ID ee23c1d21ac337c118009f257c315be5c68744d1
# Parent  7865e03a7fc1d83e9ea3c4c690a98f579a812c53
follow debugger focus;

diff -r 7865e03a7fc1 -r ee23c1d21ac3 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Mon Aug 10 14:13:49 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Mon Aug 10 14:14:49 2015 +0200
@@ -17,12 +17,16 @@
 
   sealed case class State(
     session: Session = new Session(Resources.empty),
+    focus: Option[Position.T] = None,  // position of active GUI component
     threads: Map[String, List[Debug_State]] = Map.empty,  // thread name ~> stack of debug states
     output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
   {
     def set_session(new_session: Session): State =
       copy(session = new_session)
 
+    def set_focus(new_focus: Option[Position.T]): State =
+      copy(focus = new_focus)
+
     def get_thread(thread_name: String): List[Debug_State] =
       threads.getOrElse(thread_name, Nil)
 
@@ -120,6 +124,9 @@
     current_state().session.protocol_command("Debugger.init")
   }
 
+  def focus(new_focus: Option[Position.T]): Boolean =
+    global_state.change_result(state => (state.focus != new_focus, state.set_focus(new_focus)))
+
   def cancel(thread_name: String): Unit =
     current_state().session.protocol_command("Debugger.cancel", thread_name)
 
diff -r 7865e03a7fc1 -r ee23c1d21ac3 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 14:13:49 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 14:14:49 2015 +0200
@@ -10,7 +10,8 @@
 import isabelle._
 
 import java.awt.{BorderLayout, Dimension}
-import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, MouseEvent, MouseAdapter}
+import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, MouseEvent, MouseAdapter,
+  FocusAdapter, FocusEvent}
 import javax.swing.{JTree, JScrollPane}
 import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
@@ -18,7 +19,7 @@
 import scala.swing.{Button, Label, Component, SplitPane, Orientation, CheckBox}
 import scala.swing.event.ButtonClicked
 
-import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.{jEdit, View}
 
 
 object Debugger_Dockable
@@ -117,6 +118,14 @@
 
   def thread_selection(): Option[String] = tree_selection().map(sel => sel._1.thread_name)
 
+  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.debug_states(i).pos) else None
+      case _ => None
+    }
+
   private def update_tree(thread_entries: List[Debugger_Dockable.Thread_Entry])
   {
     val old_thread_selection = thread_selection()
@@ -149,10 +158,10 @@
     tree.revalidate()
   }
 
-  private def action(node: DefaultMutableTreeNode)
-  {
-    handle_update()
-  }
+  tree.addTreeSelectionListener(
+    new TreeSelectionListener {
+      override def valueChanged(e: TreeSelectionEvent) { update_focus(focus_selection()) }
+    })
 
   tree.addMouseListener(new MouseAdapter {
     override def mouseClicked(e: MouseEvent)
@@ -161,7 +170,7 @@
       if (click != null && e.getClickCount == 1) {
         (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
           case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
-            action(node)
+            handle_update()
           case _ =>
         }
       }
@@ -212,7 +221,6 @@
       tooltip = "Evaluate ML expression within optional context"
       reactions += { case ButtonClicked(_) => eval_expression() }
     }
-  override def focusOnDefaultComponent { eval_button.requestFocus }
 
   private def eval_expression()
   {
@@ -270,6 +278,22 @@
   add(controls.peer, BorderLayout.NORTH)
 
 
+  /* focus */
+
+  override def focusOnDefaultComponent { eval_button.requestFocus }
+
+  addFocusListener(new FocusAdapter {
+    override def focusGained(e: FocusEvent) { update_focus(focus_selection()) }
+    override def focusLost(e: FocusEvent) { update_focus(None) }
+  })
+
+  private def update_focus(focus: Option[Position.T])
+  {
+    if (Debugger.focus(focus) && focus.isDefined)
+      PIDE.editor.hyperlink_position(current_snapshot, focus.get).foreach(_.follow(view))
+  }
+
+
   /* main panel */
 
   val main_panel = new SplitPane(Orientation.Vertical) {
@@ -309,6 +333,7 @@
     PIDE.session.global_options -= main
     PIDE.session.debugger_updates -= main
     delay_resize.revoke()
+    update_focus(None)
   }