| changeset 60842 | 5510c8444bc4 |
| parent 60834 | 781f1168d31e |
| child 60882 | 45bfd18835f1 |
--- a/src/Pure/PIDE/markup.scala Tue Aug 04 23:11:16 2015 +0200 +++ b/src/Pure/PIDE/markup.scala Wed Aug 05 14:18:07 2015 +0200 @@ -495,6 +495,16 @@ /* debugger output */ + val DEBUGGER_STATE = "debugger_state" + object Debugger_State + { + def unapply(props: Properties.T): Option[String] = + props match { + case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name) + case _ => None + } + } + val DEBUGGER_OUTPUT = "debugger_output" object Debugger_Output {