--- a/src/Pure/PIDE/markup.scala Thu Jan 15 11:39:58 2015 +0100
+++ b/src/Pure/PIDE/markup.scala Thu Jan 15 12:54:08 2015 +0100
@@ -471,10 +471,9 @@
val BUILD_THEORIES_RESULT = "build_theories_result"
object Build_Theories_Result
{
- def unapply(props: Properties.T): Option[(String, Boolean)] =
+ def unapply(props: Properties.T): Option[String] =
props match {
- case List((FUNCTION, BUILD_THEORIES_RESULT),
- ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
+ case List((FUNCTION, BUILD_THEORIES_RESULT), ("id", id)) => Some(id)
case _ => None
}
}