XML.pretty with depth limit;

--- a/src/Pure/General/xml.ML	Tue Jul 12 23:22:22 2011 +0200
+++ b/src/Pure/General/xml.ML	Wed Jul 13 10:57:09 2011 +0200
@@ -38,6 +38,7 @@
   val element: string -> attributes -> string list -> string
   val output_markup: Markup.T -> Output.output * Output.output
   val string_of: tree -> string
+  val pretty: int -> tree -> Pretty.T
   val output: tree -> TextIO.outstream -> unit
   val parse_comments: string list -> unit * string list
   val parse_string : string -> string option
@@ -112,19 +113,24 @@
 
 (* output *)
 
-fun buffer_of tree =
+fun buffer_of depth tree =
   let
-    fun traverse (Elem ((name, atts), [])) =
+    fun traverse _ (Elem ((name, atts), [])) =
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
-      | traverse (Elem ((name, atts), ts)) =
+      | traverse d (Elem ((name, atts), ts)) =
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
-          fold traverse ts #>
+          traverse_body d ts #>
           Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
-      | traverse (Text s) = Buffer.add (text s);
-  in Buffer.empty |> traverse tree end;
+      | traverse _ (Text s) = Buffer.add (text s)
+    and traverse_body 0 _ = Buffer.add "..."
+      | traverse_body d ts = fold (traverse (d - 1)) ts;
+  in Buffer.empty |> traverse depth tree end;
 
-val string_of = Buffer.content o buffer_of;
-val output = Buffer.output o buffer_of;
+val string_of = Buffer.content o buffer_of ~1;
+val output = Buffer.output o buffer_of ~1;
+
+fun pretty depth tree =
+  Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
 
 
 

--- a/src/Pure/ML/install_pp_polyml-5.3.ML	Tue Jul 12 23:22:22 2011 +0200
+++ b/src/Pure/ML/install_pp_polyml-5.3.ML	Wed Jul 13 10:57:09 2011 +0200
@@ -7,6 +7,9 @@
 PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
   ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
 
+PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
+  ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
+
 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
   pretty (Synchronized.value var, depth));
 

--- a/src/Pure/ROOT.ML	Tue Jul 12 23:22:22 2011 +0200
+++ b/src/Pure/ROOT.ML	Wed Jul 13 10:57:09 2011 +0200
@@ -52,8 +52,8 @@
 use "General/graph.ML";
 use "General/linear_set.ML";
 use "General/buffer.ML";
+use "General/pretty.ML";
 use "General/xml.ML";
-use "General/pretty.ML";
 use "General/path.ML";
 use "General/url.ML";
 use "General/file.ML";

--- a/src/Pure/pure_setup.ML	Tue Jul 12 23:22:22 2011 +0200
+++ b/src/Pure/pure_setup.ML	Wed Jul 13 10:57:09 2011 +0200
@@ -18,7 +18,6 @@
 
 (* ML toplevel pretty printing *)
 
-toplevel_pp ["XML", "tree"] "Pretty.str o XML.string_of";
 toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
 toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";