src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Tue Feb 18 15:38:50 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Feb 18 16:34:02 2014 +0100
@@ -67,6 +67,20 @@
   val POSITION = "position"
 
 
+  /* embedded languages */
+
+  val LANGUAGE = "language"
+
+  object Language
+  {
+    def unapply(markup: Markup): Option[String] =
+      markup match {
+        case Markup(LANGUAGE, Name(name)) => Some(name)
+        case _ => None
+      }
+  }
+
+
   /* external resources */
 
   val PATH = "path"
@@ -138,11 +152,6 @@
 
   val TOKEN_RANGE = "token_range"
 
-  val SORT = "sort"
-  val TYP = "typ"
-  val TERM = "term"
-  val PROP = "prop"
-
   val SORTING = "sorting"
   val TYPING = "typing"
 
@@ -150,10 +159,7 @@
   val METHOD = "method"
 
 
-  /* embedded source text */
-
-  val ML_SOURCE = "ML_source"
-  val DOCUMENT_SOURCE = "document_source"
+  /* antiquotations */
 
   val ANTIQUOTED = "antiquoted"
   val ANTIQUOTE = "antiquote"