src/Pure/PIDE/markup.scala
changeset 55616 25a7a998852a
parent 55615 bf4bbe72f740
child 55666 cc350eb1087e
     1.1 --- a/src/Pure/PIDE/markup.scala	Thu Feb 20 12:53:12 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Feb 20 13:23:49 2014 +0100
     1.3 @@ -93,6 +93,9 @@
     1.4    val LANGUAGE = "language"
     1.5    object Language
     1.6    {
     1.7 +    val ML = "ML"
     1.8 +    val UNKNOWN = "unknown"
     1.9 +
    1.10      def unapply(markup: Markup): Option[(String, Boolean)] =
    1.11        markup match {
    1.12          case Markup(LANGUAGE, props) =>