src/Pure/PIDE/markup.scala
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
   {