src/Pure/PIDE/markup.scala
changeset 59369 7090199d3f78
parent 59367 6193bbbbe564
child 59707 10effab11669
     1.1 --- a/src/Pure/PIDE/markup.scala	Thu Jan 15 11:39:58 2015 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Jan 15 12:54:08 2015 +0100
     1.3 @@ -471,10 +471,9 @@
     1.4    val BUILD_THEORIES_RESULT = "build_theories_result"
     1.5    object Build_Theories_Result
     1.6    {
     1.7 -    def unapply(props: Properties.T): Option[(String, Boolean)] =
     1.8 +    def unapply(props: Properties.T): Option[String] =
     1.9        props match {
    1.10 -        case List((FUNCTION, BUILD_THEORIES_RESULT),
    1.11 -          ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
    1.12 +        case List((FUNCTION, BUILD_THEORIES_RESULT), ("id", id)) => Some(id)
    1.13          case _ => None
    1.14        }
    1.15    }