src/Pure/Tools/debugger.scala

--- a/src/Pure/Tools/debugger.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Tools/debugger.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -23,7 +23,7 @@
   {
     def size: Int = debug_states.length + 1
     def reset: Context = copy(index = 0)
-    def select(i: Int) = copy(index = i + 1)
+    def select(i: Int): Context = copy(index = i + 1)
 
     def thread_state: Option[Debug_State] = debug_states.headOption
 
@@ -143,8 +143,8 @@
 
     val functions =
       List(
-        Markup.DEBUGGER_STATE -> debugger_state _,
-        Markup.DEBUGGER_OUTPUT -> debugger_output _)
+        Markup.DEBUGGER_STATE -> debugger_state,
+        Markup.DEBUGGER_OUTPUT -> debugger_output)
   }
 }