src/Pure/PIDE/markup.scala
changeset 56616 abc2da18d08d
parent 56548 ae6870efc28d
child 56623 4675df68450e
     1.1 --- a/src/Pure/PIDE/markup.scala	Thu Apr 17 12:03:15 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Apr 17 13:21:36 2014 +0200
     1.3 @@ -420,6 +420,25 @@
     1.4        }
     1.5    }
     1.6  
     1.7 +  object Loading_Theory
     1.8 +  {
     1.9 +    def unapply(props: Properties.T): Option[String] =
    1.10 +      props match {
    1.11 +        case List((FUNCTION, "loading_theory"), (NAME, name)) => Some(name)
    1.12 +        case _ => None
    1.13 +      }
    1.14 +  }
    1.15 +
    1.16 +  object Use_Theories_Result
    1.17 +  {
    1.18 +    def unapply(props: Properties.T): Option[(String, Boolean)] =
    1.19 +      props match {
    1.20 +        case List((FUNCTION, "use_theories_result"),
    1.21 +          ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
    1.22 +        case _ => None
    1.23 +      }
    1.24 +  }
    1.25 +
    1.26  
    1.27    /* simplifier trace */
    1.28