src/Pure/PIDE/markup.scala
changeset 59369 7090199d3f78
parent 59367 6193bbbbe564
child 59707 10effab11669
--- 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
       }
   }