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
       }
   }