src/Pure/PIDE/markup.scala
changeset 55552 bcc643ac071a
parent 55526 39708e59f4b0
child 55553 4a5f65df29fa
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Feb 18 15:38:50 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Feb 18 16:34:02 2014 +0100
     1.3 @@ -67,6 +67,20 @@
     1.4    val POSITION = "position"
     1.5  
     1.6  
     1.7 +  /* embedded languages */
     1.8 +
     1.9 +  val LANGUAGE = "language"
    1.10 +
    1.11 +  object Language
    1.12 +  {
    1.13 +    def unapply(markup: Markup): Option[String] =
    1.14 +      markup match {
    1.15 +        case Markup(LANGUAGE, Name(name)) => Some(name)
    1.16 +        case _ => None
    1.17 +      }
    1.18 +  }
    1.19 +
    1.20 +
    1.21    /* external resources */
    1.22  
    1.23    val PATH = "path"
    1.24 @@ -138,11 +152,6 @@
    1.25  
    1.26    val TOKEN_RANGE = "token_range"
    1.27  
    1.28 -  val SORT = "sort"
    1.29 -  val TYP = "typ"
    1.30 -  val TERM = "term"
    1.31 -  val PROP = "prop"
    1.32 -
    1.33    val SORTING = "sorting"
    1.34    val TYPING = "typing"
    1.35  
    1.36 @@ -150,10 +159,7 @@
    1.37    val METHOD = "method"
    1.38  
    1.39  
    1.40 -  /* embedded source text */
    1.41 -
    1.42 -  val ML_SOURCE = "ML_source"
    1.43 -  val DOCUMENT_SOURCE = "document_source"
    1.44 +  /* antiquotations */
    1.45  
    1.46    val ANTIQUOTED = "antiquoted"
    1.47    val ANTIQUOTE = "antiquote"