diff -r 7e8f4df04d5d -r a942e237c9e8 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sat Dec 19 23:25:23 2015 +0100
+++ b/src/Pure/General/pretty.scala	Sun Dec 20 12:48:56 2015 +0100
@@ -11,8 +11,11 @@
 {
   /* XML constructors */
 
-  def spaces(n: Int): XML.Body = if (n == 0) Nil else List(XML.Text(Symbol.spaces(n)))
-  val space: XML.Body = spaces(1)
+  val space: XML.Body = List(XML.Text(Symbol.space))
+  def spaces(n: Int): XML.Body =
+    if (n == 0) Nil
+    else if (n == 1) space
+    else List(XML.Text(Symbol.spaces(n)))
 
   def block(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
     XML.Elem(Markup.Block(consistent, indent), body)
@@ -45,79 +48,79 @@
 
   /* markup trees with physical blocks and breaks */
 
-  sealed abstract class Tree { def length: Double }
-  case class Block(
+  private sealed abstract class Tree { def length: Double }
+  private case class Block(
     markup: Option[(Markup, Option[XML.Body])],
     consistent: Boolean, indent: Int, body: List[Tree], length: Double) extends Tree
-  case class Str(string: String, length: Double) extends Tree
-  case class Break(force: Boolean, width: Int, indent: Int) extends Tree
+  private case class Break(force: Boolean, width: Int, indent: Int) extends Tree
   { def length: Double = width.toDouble }
+  private case class Str(string: String, length: Double) extends Tree
 
-  val FBreak = Break(true, 1, 0)
+  private val FBreak = Break(true, 1, 0)
 
-  def make_block(
+  private def make_block(
       markup: Option[(Markup, Option[XML.Body])],
       consistent: Boolean,
       indent: Int,
       body: List[Tree]): Tree =
     Block(markup, consistent, indent, body, (0.0 /: body) { case (n, t) => n + t.length })
 
-  def make_tree(metric: Metric, xml: XML.Body): List[Tree] =
-    xml flatMap {
-      case XML.Wrapped_Elem(markup, body1, body2) =>
-        List(make_block(Some(markup, Some(body1)), false, 0, make_tree(metric, body2)))
-      case XML.Elem(markup, body) =>
-        markup match {
-          case Markup.Block(consistent, indent) =>
-            List(make_block(None, consistent, indent, make_tree(metric, body)))
-          case Markup.Break(width, indent) =>
-            List(Break(false, width, indent))
-          case Markup(Markup.ITEM, _) =>
-            List(make_block(None, false, 2,
-              make_tree(metric, XML.elem(Markup.BULLET, space) :: space ::: body)))
-          case _ =>
-            List(make_block(Some((markup, None)), false, 0, make_tree(metric, body)))
-        }
-      case XML.Text(text) =>
-        Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s))))
+
+  /* formatted output */
+
+  private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
+  {
+    def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)
+    def string(s: String, len: Double): Text =
+      copy(tx = if (s == "") tx else XML.Text(s) :: tx, pos = pos + len)
+    def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
+    def content: XML.Body = tx.reverse
+  }
+
+  private def break_dist(trees: List[Tree], after: Double): Double =
+    trees match {
+      case (_: Break) :: _ => 0.0
+      case t :: ts => t.length + break_dist(ts, after)
+      case Nil => after
     }
 
+  private def force_break(tree: Tree): Tree =
+    tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
+  private def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break(_))
 
-  /* formatted output */
+  private def force_next(trees: List[Tree]): List[Tree] =
+    trees match {
+      case Nil => Nil
+      case (t: Break) :: ts => force_break(t) :: ts
+      case t :: ts => t :: force_next(ts)
+    }
 
   private val margin_default = 76.0
 
   def formatted(input: XML.Body, margin: Double = margin_default,
     metric: Metric = Metric_Default): XML.Body =
   {
-    sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
-    {
-      def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)
-      def string(s: String, len: Double): Text =
-        copy(tx = if (s == "") tx else XML.Text(s) :: tx, pos = pos + len)
-      def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
-      def content: XML.Body = tx.reverse
-    }
-
     val breakgain = margin / 20
     val emergencypos = (margin / 2).round.toInt
 
-    def break_dist(trees: List[Tree], after: Double): Double =
-      trees match {
-        case (_: Break) :: _ => 0.0
-        case t :: ts => t.length + break_dist(ts, after)
-        case Nil => after
-      }
-
-    def force_break(tree: Tree): Tree =
-      tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
-    def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break(_))
-
-    def force_next(trees: List[Tree]): List[Tree] =
-      trees match {
-        case Nil => Nil
-        case (t: Break) :: ts => force_break(t) :: ts
-        case t :: ts => t :: force_next(ts)
+    def make_tree(inp: XML.Body): List[Tree] =
+      inp flatMap {
+        case XML.Wrapped_Elem(markup, body1, body2) =>
+          List(make_block(Some(markup, Some(body1)), false, 0, make_tree(body2)))
+        case XML.Elem(markup, body) =>
+          markup match {
+            case Markup.Block(consistent, indent) =>
+              List(make_block(None, consistent, indent, make_tree(body)))
+            case Markup.Break(width, indent) =>
+              List(Break(false, width, indent))
+            case Markup(Markup.ITEM, _) =>
+              List(make_block(None, false, 2,
+                make_tree(XML.elem(Markup.BULLET, space) :: space ::: body)))
+            case _ =>
+              List(make_block(Some((markup, None)), false, 0, make_tree(body)))
+          }
+        case XML.Text(text) =>
+          Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s))))
       }
 
     def format(trees: List[Tree], blockin: Int, after: Double, text: Text): Text =
@@ -153,7 +156,7 @@
 
         case Str(s, len) :: ts => format(ts, blockin, after, text.string(s, len))
       }
-    format(make_tree(metric, input), 0, 0.0, Text()).content
+    format(make_tree(input), 0, 0.0, Text()).content
   }
 
   def string_of(input: XML.Body, margin: Double = margin_default,