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