src/Pure/PIDE/markup.scala
changeset 59366 e94df7f6b608
parent 59364 3b5da177ae6b
child 59367 6193bbbbe564
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed Jan 14 16:23:33 2015 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jan 14 16:27:19 2015 +0100
     1.3 @@ -467,11 +467,12 @@
     1.4        }
     1.5    }
     1.6  
     1.7 +  val BUILD_THEORIES_RESULT = "build_theories_result"
     1.8    object Build_Theories_Result
     1.9    {
    1.10      def unapply(props: Properties.T): Option[(String, Boolean)] =
    1.11        props match {
    1.12 -        case List((FUNCTION, "build_theories_result"),
    1.13 +        case List((FUNCTION, BUILD_THEORIES_RESULT),
    1.14            ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
    1.15          case _ => None
    1.16        }