1.1 --- a/src/Pure/General/markup.scala	Wed Aug 25 22:45:24 2010 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Wed Aug 25 22:57:40 2010 +0200
     1.3 @@ -94,9 +94,9 @@
     1.4  
     1.5    /* pretty printing */
     1.6  
     1.7 -  val INDENT = "indent"
     1.8 +  val Indent = new Int_Property("indent")
     1.9    val BLOCK = "block"
    1.10 -  val WIDTH = "width"
    1.11 +  val Width = new Int_Property("width")
    1.12    val BREAK = "break"
    1.13  
    1.14  

     2.1 --- a/src/Pure/General/pretty.scala	Wed Aug 25 22:45:24 2010 +0200
     2.2 +++ b/src/Pure/General/pretty.scala	Wed Aug 25 22:57:40 2010 +0200
     2.3 @@ -19,12 +19,11 @@
     2.4    object Block
     2.5    {
     2.6      def apply(i: Int, body: XML.Body): XML.Tree =
     2.7 -      XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body)
     2.8 +      XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
     2.9  
    2.10      def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
    2.11        tree match {
    2.12 -        case XML.Elem(
    2.13 -          Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body) => Some((i, body))
    2.14 +        case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) => Some((i, body))
    2.15          case _ => None
    2.16        }
    2.17    }
    2.18 @@ -32,12 +31,11 @@
    2.19    object Break
    2.20    {
    2.21      def apply(w: Int): XML.Tree =
    2.22 -      XML.Elem(
    2.23 -        Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), List(XML.Text(Symbol.spaces(w))))
    2.24 +      XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), List(XML.Text(Symbol.spaces(w))))
    2.25  
    2.26      def unapply(tree: XML.Tree): Option[Int] =
    2.27        tree match {
    2.28 -        case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), _) => Some(w)
    2.29 +        case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
    2.30          case _ => None
    2.31        }
    2.32    }