src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Wed Feb 19 21:38:44 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Feb 20 12:53:12 2014 +0100
@@ -59,7 +59,7 @@
       markup match {
         case Markup(ENTITY, props) =>
           (props, props) match {
-            case (Kind(kind), Name(name)) => Some(kind, name)
+            case (Kind(kind), Name(name)) => Some((kind, name))
             case _ => None
           }
         case _ => None
@@ -87,8 +87,22 @@
 
   /* embedded languages */
 
+  val SYMBOLS = "symbols"
+  val Symbols = new Properties.Boolean(SYMBOLS)
+
   val LANGUAGE = "language"
-  val Language = new Markup_String(LANGUAGE, NAME)
+  object Language
+  {
+    def unapply(markup: Markup): Option[(String, Boolean)] =
+      markup match {
+        case Markup(LANGUAGE, props) =>
+          (props, props) match {
+            case (Name(name), Symbols(symbols)) => Some((name, symbols))
+            case _ => None
+          }
+        case _ => None
+      }
+  }
 
 
   /* external resources */