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)