# HG changeset patch
# User wenzelm
# Date 1282769860 -7200
# Node ID d1feec02cf0205a826542c2cf7a39f2e457aee22
# Parent  6a55b8978a5669ba53a5a139f5a6240b1e7362c9
Pretty: tuned markup objects;

diff -r 6a55b8978a56 -r d1feec02cf02 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Wed Aug 25 22:45:24 2010 +0200
+++ b/src/Pure/General/markup.scala	Wed Aug 25 22:57:40 2010 +0200
@@ -94,9 +94,9 @@
 
   /* pretty printing */
 
-  val INDENT = "indent"
+  val Indent = new Int_Property("indent")
   val BLOCK = "block"
-  val WIDTH = "width"
+  val Width = new Int_Property("width")
   val BREAK = "break"
 
 
diff -r 6a55b8978a56 -r d1feec02cf02 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Wed Aug 25 22:45:24 2010 +0200
+++ b/src/Pure/General/pretty.scala	Wed Aug 25 22:57:40 2010 +0200
@@ -19,12 +19,11 @@
   object Block
   {
     def apply(i: Int, body: XML.Body): XML.Tree =
-      XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body)
+      XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
 
     def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
       tree match {
-        case XML.Elem(
-          Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body) => Some((i, body))
+        case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) => Some((i, body))
         case _ => None
       }
   }
@@ -32,12 +31,11 @@
   object Break
   {
     def apply(w: Int): XML.Tree =
-      XML.Elem(
-        Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), List(XML.Text(Symbol.spaces(w))))
+      XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), List(XML.Text(Symbol.spaces(w))))
 
     def unapply(tree: XML.Tree): Option[Int] =
       tree match {
-        case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), _) => Some(w)
+        case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
         case _ => None
       }
   }