diff -r 100db5cf5be5 -r 7090199d3f78 src/Pure/PIDE/markup.scala --- 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 } }