diff -r bff9c05fe229 -r f76ad0771f67 src/Pure/ML-Systems/ml_pretty.ML
--- a/src/Pure/ML-Systems/ml_pretty.ML	Mon Aug 23 12:06:47 2010 +0200
+++ b/src/Pure/ML-Systems/ml_pretty.ML	Mon Aug 23 15:11:41 2010 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML-Systems/ml_pretty.ML
     Author:     Makarius
 
-Raw datatype for ML pretty printing.
+Minimal support for raw ML pretty printing -- for boot-strapping only.
 *)
 
 structure ML_Pretty =
@@ -12,5 +12,20 @@
   String of string * int |
   Break of bool * int;
 
+fun block prts = Block (("", ""), prts, 2);
+fun str s = String (s, size s);
+fun brk wd = Break (false, wd);
+
+fun pair pretty1 pretty2 ((x, y), depth: int) =
+  block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
+
+fun enum sep lpar rpar pretty (args, depth) =
+  let
+    fun elems _ [] = []
+      | elems 0 _ = [str "..."]
+      | elems d [x] = [pretty (x, d)]
+      | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
+  in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
+
 end;