# HG changeset patch
# User wenzelm
# Date 1392739392 -3600
# Node ID 4a5f65df29fac9185355b2c2a58840cc030d2393
# Parent  bcc643ac071a7c643bcb207ce503153bfda14166
tuned signature;

diff -r bcc643ac071a -r 4a5f65df29fa src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Tue Feb 18 16:34:02 2014 +0100
+++ b/src/Pure/General/pretty.scala	Tue Feb 18 17:03:12 2014 +0100
@@ -45,12 +45,11 @@
   object Block
   {
     def apply(i: Int, body: XML.Body): XML.Tree =
-      XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
+      XML.Elem(Markup.Block(i), body)
 
     def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
       tree match {
-        case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) =>
-          Some((i, body))
+        case XML.Elem(Markup.Block(i), body) => Some((i, body))
         case _ => None
       }
   }
@@ -58,12 +57,11 @@
   object Break
   {
     def apply(w: Int): XML.Tree =
-      XML.Elem(Markup(Markup.BREAK, Markup.Width(w)),
-        List(XML.Text(spaces(w))))
+      XML.Elem(Markup.Break(w), List(XML.Text(spaces(w))))
 
     def unapply(tree: XML.Tree): Option[Int] =
       tree match {
-        case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
+        case XML.Elem(Markup.Break(w), _) => Some(w)
         case _ => None
       }
   }
diff -r bcc643ac071a -r 4a5f65df29fa src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Feb 18 16:34:02 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Feb 18 17:03:12 2014 +0100
@@ -221,9 +221,9 @@
 fun properties more_props ((elem, props): T) =
   (elem, fold_rev Properties.put more_props props);
 
-fun markup_elem elem = (elem, (elem, []): T);
-fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
-fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
+fun markup_elem name = (name, (name, []): T);
+fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T);
+fun markup_int name prop = (name, fn i => (name, [(prop, print_int i)]): T);
 
 
 (* misc properties *)
diff -r bcc643ac071a -r 4a5f65df29fa src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Feb 18 16:34:02 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Feb 18 17:03:12 2014 +0100
@@ -27,6 +27,24 @@
   val Empty = Markup("", Nil)
   val Broken = Markup("broken", Nil)
 
+  class Markup_String(val name: String, prop: String)
+  {
+    private val Prop = new Properties.String(prop)
+
+    def apply(s: String): Markup = Markup(name, Prop(s))
+    def unapply(markup: Markup): Option[String] =
+      if (markup.name == name) Prop.unapply(markup.properties) else None
+  }
+
+  class Markup_Int(val name: String, prop: String)
+  {
+    private val Prop = new Properties.Int(prop)
+
+    def apply(i: Int): Markup = Markup(name, Prop(i))
+    def unapply(markup: Markup): Option[Int] =
+      if (markup.name == name) Prop.unapply(markup.properties) else None
+  }
+
 
   /* formal entities */
 
@@ -39,9 +57,9 @@
   {
     def unapply(markup: Markup): Option[(String, String)] =
       markup match {
-        case Markup(ENTITY, props @ Kind(kind)) =>
-          props match {
-            case Name(name) => Some(kind, name)
+        case Markup(ENTITY, props) =>
+          (props, props) match {
+            case (Kind(kind), Name(name)) => Some(kind, name)
             case _ => None
           }
         case _ => None
@@ -70,49 +88,22 @@
   /* embedded languages */
 
   val LANGUAGE = "language"
-
-  object Language
-  {
-    def unapply(markup: Markup): Option[String] =
-      markup match {
-        case Markup(LANGUAGE, Name(name)) => Some(name)
-        case _ => None
-      }
-  }
+  val Language = new Markup_String(LANGUAGE, NAME)
 
 
   /* external resources */
 
   val PATH = "path"
-
-  object Path
-  {
-    def unapply(markup: Markup): Option[String] =
-      markup match {
-        case Markup(PATH, Name(name)) => Some(name)
-        case _ => None
-      }
-  }
+  val Path = new Markup_String(PATH, NAME)
 
   val URL = "url"
-
-  object Url
-  {
-    def unapply(markup: Markup): Option[String] =
-      markup match {
-        case Markup(URL, Name(name)) => Some(name)
-        case _ => None
-      }
-  }
+  val Url = new Markup_String(URL, NAME)
 
 
   /* pretty printing */
 
-  val Indent = new Properties.Int("indent")
-  val BLOCK = "block"
-
-  val Width = new Properties.Int("width")
-  val BREAK = "break"
+  val Block = new Markup_Int("block", "indent")
+  val Break = new Markup_Int("break", "width")
 
   val ITEM = "item"
   val BULLET = "bullet"
diff -r bcc643ac071a -r 4a5f65df29fa src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala	Tue Feb 18 16:34:02 2014 +0100
+++ b/src/Pure/PIDE/yxml.scala	Tue Feb 18 17:03:12 2014 +0100
@@ -120,7 +120,7 @@
   /* failsafe parsing */
 
   private def markup_broken(source: CharSequence) =
-    XML.elem(Markup.Broken.name, List(XML.Text(source.toString)))
+    XML.Elem(Markup.Broken, List(XML.Text(source.toString)))
 
   def parse_body_failsafe(source: CharSequence): XML.Body =
   {