src/Pure/Tools/debugger.scala

--- a/src/Pure/Tools/debugger.scala	Tue Aug 11 18:42:29 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Tue Aug 11 20:05:27 2015 +0200
@@ -195,4 +195,12 @@
       state.clear_output(thread_name)
     })
   }
+
+  def print_vals(thread_name: String, index: Int, SML: Boolean, context: String)
+  {
+    global_state.change(state => {
+      input(thread_name, "print_vals", index.toString, SML.toString, Symbol.encode(context))
+      state.clear_output(thread_name)
+    })
+  }
 }