src/Pure/General/xml.ML
changeset 43791 5e9a1d71f94d
parent 43783 ef45eaf2775f
child 43797 fad7758421bf
     1.1 --- a/src/Pure/General/xml.ML	Tue Jul 12 23:22:22 2011 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Wed Jul 13 10:57:09 2011 +0200
     1.3 @@ -38,6 +38,7 @@
     1.4    val element: string -> attributes -> string list -> string
     1.5    val output_markup: Markup.T -> Output.output * Output.output
     1.6    val string_of: tree -> string
     1.7 +  val pretty: int -> tree -> Pretty.T
     1.8    val output: tree -> TextIO.outstream -> unit
     1.9    val parse_comments: string list -> unit * string list
    1.10    val parse_string : string -> string option
    1.11 @@ -112,19 +113,24 @@
    1.12  
    1.13  (* output *)
    1.14  
    1.15 -fun buffer_of tree =
    1.16 +fun buffer_of depth tree =
    1.17    let
    1.18 -    fun traverse (Elem ((name, atts), [])) =
    1.19 +    fun traverse _ (Elem ((name, atts), [])) =
    1.20            Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
    1.21 -      | traverse (Elem ((name, atts), ts)) =
    1.22 +      | traverse d (Elem ((name, atts), ts)) =
    1.23            Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
    1.24 -          fold traverse ts #>
    1.25 +          traverse_body d ts #>
    1.26            Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
    1.27 -      | traverse (Text s) = Buffer.add (text s);
    1.28 -  in Buffer.empty |> traverse tree end;
    1.29 +      | traverse _ (Text s) = Buffer.add (text s)
    1.30 +    and traverse_body 0 _ = Buffer.add "..."
    1.31 +      | traverse_body d ts = fold (traverse (d - 1)) ts;
    1.32 +  in Buffer.empty |> traverse depth tree end;
    1.33  
    1.34 -val string_of = Buffer.content o buffer_of;
    1.35 -val output = Buffer.output o buffer_of;
    1.36 +val string_of = Buffer.content o buffer_of ~1;
    1.37 +val output = Buffer.output o buffer_of ~1;
    1.38 +
    1.39 +fun pretty depth tree =
    1.40 +  Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
    1.41  
    1.42  
    1.43