src/Pure/PIDE/markup.scala
changeset 60842 5510c8444bc4
parent 60834 781f1168d31e
child 60882 45bfd18835f1
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Aug 04 23:11:16 2015 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Wed Aug 05 14:18:07 2015 +0200
     1.3 @@ -495,6 +495,16 @@
     1.4  
     1.5    /* debugger output */
     1.6  
     1.7 +  val DEBUGGER_STATE = "debugger_state"
     1.8 +  object Debugger_State
     1.9 +  {
    1.10 +    def unapply(props: Properties.T): Option[String] =
    1.11 +      props match {
    1.12 +        case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name)
    1.13 +        case _ => None
    1.14 +      }
    1.15 +  }
    1.16 +
    1.17    val DEBUGGER_OUTPUT = "debugger_output"
    1.18    object Debugger_Output
    1.19    {