src/Pure/Tools/debugger.scala

--- 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)
     })