src/Pure/PIDE/markup.scala
changeset 60834 781f1168d31e
parent 60831 5b99a334fd4c
child 60842 5510c8444bc4
     1.1 --- a/src/Pure/PIDE/markup.scala	Thu Jul 30 11:32:58 2015 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Jul 30 11:39:30 2015 +0200
     1.3 @@ -498,10 +498,9 @@
     1.4    val DEBUGGER_OUTPUT = "debugger_output"
     1.5    object Debugger_Output
     1.6    {
     1.7 -    def unapply(props: Properties.T): Option[(String, Long)] =
     1.8 +    def unapply(props: Properties.T): Option[String] =
     1.9        props match {
    1.10 -        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name), (SERIAL, Properties.Value.Long(i))) =>
    1.11 -          Some((name, i))
    1.12 +        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
    1.13          case _ => None
    1.14        }
    1.15    }