--- a/src/Pure/PIDE/markup.scala Thu Jul 30 11:32:58 2015 +0200
+++ b/src/Pure/PIDE/markup.scala Thu Jul 30 11:39:30 2015 +0200
@@ -498,10 +498,9 @@
val DEBUGGER_OUTPUT = "debugger_output"
object Debugger_Output
{
- def unapply(props: Properties.T): Option[(String, Long)] =
+ def unapply(props: Properties.T): Option[String] =
props match {
- case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name), (SERIAL, Properties.Value.Long(i))) =>
- Some((name, i))
+ case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
case _ => None
}
}