diff -r 4b16b778ce0d -r f56e189350b2 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Wed Jul 29 11:41:26 2015 +0200 +++ b/src/Pure/PIDE/markup.scala Wed Jul 29 13:34:04 2015 +0200 @@ -493,6 +493,20 @@ val PRINT_OPERATIONS = "print_operations" + /* debugger output */ + + val DEBUGGER_OUTPUT = "debugger_output" + object Debugger_Output + { + def unapply(props: Properties.T): Option[(String, Long)] = + props match { + case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name), (SERIAL, Properties.Value.Long(i))) => + Some((name, i)) + case _ => None + } + } + + /* simplifier trace */ val SIMP_TRACE_PANEL = "simp_trace_panel"