changeset 60897 | 7aad4be8a48e |
parent 60896 | 625f2c8307da |
child 60898 | a3fcde62df10 |
--- 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) + }) + } }