maintain per-thread focus context;
tuned signature;

--- a/src/Pure/Tools/debugger.scala	Mon Aug 24 00:20:20 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Mon Aug 24 11:38:05 2015 +0200
@@ -28,12 +28,13 @@
         Some(debug_states(index - 1))
       else None
 
-    def debug_state_index: Option[Int] =
+    def debug_index: Option[Int] =
       if (stack_state.isDefined) Some(index - 1)
       else if (debug_states.nonEmpty) Some(0)
       else None
 
     def debug_state: Option[Debug_State] = stack_state orElse thread_state
+    def debug_position: Option[Position.T] = debug_state.map(_.pos)
 
     override def toString: String =
       stack_state match {
@@ -50,8 +51,8 @@
     active: Int = 0,  // active views
     break: Boolean = false,  // break at next possible breakpoint
     active_breakpoints: Set[Long] = Set.empty,  // explicit breakpoint state
-    focus: Option[Position.T] = None,  // position of active GUI component
     threads: Map[String, List[Debug_State]] = Map.empty,  // thread name ~> stack of debug states
+    focus: Map[String, Context] = Map.empty,  // thread name ~> focus
     output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
   {
     def set_session(new_session: Session): State =
@@ -71,16 +72,15 @@
       (active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1))
     }
 
-    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)
 
     def update_thread(thread_name: String, debug_states: List[Debug_State]): State =
-      if (debug_states.isEmpty) copy(threads = threads - thread_name)
+      if (debug_states.isEmpty) copy(threads = threads - thread_name, focus = focus - thread_name)
       else copy(threads = threads + (thread_name -> debug_states))
 
+    def set_focus(c: Context): State = copy(focus = focus + (c.thread_name -> c))
+
     def get_output(thread_name: String): Command.Results =
       output.getOrElse(thread_name, Command.Results.empty)
 
@@ -222,16 +222,15 @@
     })
   }
 
-  def focus(): Option[Position.T] = global_state.value.focus
+  def threads(): Map[String, List[Debug_State]] = global_state.value.threads
 
-  def set_focus(focus: Option[Position.T])
+  def focus(): List[Context] = global_state.value.focus.toList.map(_._2)
+  def set_focus(c: Context)
   {
-    global_state.change(_.set_focus(focus))
+    global_state.change(_.set_focus(c))
     delay_update.invoke()
   }
 
-  def threads(): Map[String, List[Debug_State]] = global_state.value.threads
-
   def output(): Map[String, Command.Results] = global_state.value.output
 
   def input(thread_name: String, msg: String*): Unit =
@@ -251,7 +250,7 @@
   def eval(c: Context, SML: Boolean, context: String, expression: String)
   {
     global_state.change(state => {
-      input(c.thread_name, "eval", c.debug_state_index.getOrElse(0).toString,
+      input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString,
         SML.toString, Symbol.encode(context), Symbol.encode(expression))
       state.clear_output(c.thread_name)
     })
@@ -260,10 +259,10 @@
 
   def print_vals(c: Context, SML: Boolean, context: String)
   {
-    require(c.debug_state_index.isDefined)
+    require(c.debug_index.isDefined)
 
     global_state.change(state => {
-      input(c.thread_name, "print_vals", c.debug_state_index.getOrElse(0).toString,
+      input(c.thread_name, "print_vals", c.debug_index.getOrElse(0).toString,
         SML.toString, Symbol.encode(context))
       state.clear_output(c.thread_name)
     })

--- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 24 00:20:20 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 24 11:38:05 2015 +0200
@@ -141,12 +141,6 @@
 
   def thread_selection(): Option[String] = tree_selection().map(_.thread_name)
 
-  def focus_selection(): Option[Position.T] =
-    for {
-      c <- tree_selection()
-      d <- c.debug_state
-    } yield d.pos
-
   private def update_tree(threads: List[Debugger.Context])
   {
     require(threads.forall(_.index == 0))
@@ -199,7 +193,7 @@
   tree.addTreeSelectionListener(
     new TreeSelectionListener {
       override def valueChanged(e: TreeSelectionEvent) {
-        update_focus(focus_selection())
+        update_focus()
         update_vals()
       }
     })
@@ -209,7 +203,7 @@
       {
         val click = tree.getPathForLocation(e.getX, e.getY)
         if (click != null && e.getClickCount == 1)
-          update_focus(focus_selection())
+          update_focus()
       }
     })
 
@@ -292,7 +286,7 @@
     context_field.addCurrentToHistory()
     expression_field.addCurrentToHistory()
     tree_selection() match {
-      case Some(c) if c.debug_state_index.isDefined =>
+      case Some(c) if c.debug_index.isDefined =>
         Debugger.eval(c, sml_button.selected, context_field.getText, expression_field.getText)
       case _ =>
     }
@@ -319,16 +313,21 @@
   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) }
+    override def focusGained(e: FocusEvent) { update_focus() }
   })
 
-  private def update_focus(focus: Option[Position.T])
+  private def update_focus()
   {
-    Debugger.set_focus(focus)
-    if (focus.isDefined)
-      PIDE.editor.hyperlink_position(false, current_snapshot, focus.get).foreach(_.follow(view))
-    view.getTextArea.repaint()
+    for (c <- tree_selection()) {
+      Debugger.set_focus(c)
+      for {
+        pos <- c.debug_position
+        link <- PIDE.editor.hyperlink_position(false, current_snapshot, pos)
+      } {
+        link.follow(view)
+        view.getTextArea.repaint()
+      }
+    }
   }
 
 
@@ -370,7 +369,6 @@
     PIDE.session.global_options -= main
     PIDE.session.debugger_updates -= main
     delay_resize.revoke()
-    update_focus(None)
     Debugger.exit()
     jEdit.propertiesChanged()
   }

--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 24 00:20:20 2015 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 24 11:38:05 2015 +0200
@@ -352,10 +352,16 @@
   private def caret_color(rendering: Rendering, offset: Text.Offset): Color =
   {
     if (text_area.isCaretVisible) text_area.getPainter.getCaretColor
-    else
-      if (Debugger.focus().exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _)))
+    else {
+      val debug_positions =
+        for {
+          c <- Debugger.focus()
+          pos <- c.debug_position
+        } yield pos
+      if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _)))
         rendering.caret_debugger_color
       else rendering.caret_invisible_color
+    }
   }
 
   private def paint_chunk_list(rendering: Rendering,