XML.pretty with depth limit;
authorwenzelm
Wed Jul 13 10:57:09 2011 +0200 (2011-07-13)
changeset 437915e9a1d71f94d
parent 43790 9bd8d4addd6e
child 43792 d5803c3d537a
XML.pretty with depth limit;
src/Pure/General/xml.ML
src/Pure/ML/install_pp_polyml-5.3.ML
src/Pure/ROOT.ML
src/Pure/pure_setup.ML
     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  
     2.1 --- a/src/Pure/ML/install_pp_polyml-5.3.ML	Tue Jul 12 23:22:22 2011 +0200
     2.2 +++ b/src/Pure/ML/install_pp_polyml-5.3.ML	Wed Jul 13 10:57:09 2011 +0200
     2.3 @@ -7,6 +7,9 @@
     2.4  PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
     2.5    ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
     2.6  
     2.7 +PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
     2.8 +  ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
     2.9 +
    2.10  PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
    2.11    pretty (Synchronized.value var, depth));
    2.12  
     3.1 --- a/src/Pure/ROOT.ML	Tue Jul 12 23:22:22 2011 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Wed Jul 13 10:57:09 2011 +0200
     3.3 @@ -52,8 +52,8 @@
     3.4  use "General/graph.ML";
     3.5  use "General/linear_set.ML";
     3.6  use "General/buffer.ML";
     3.7 +use "General/pretty.ML";
     3.8  use "General/xml.ML";
     3.9 -use "General/pretty.ML";
    3.10  use "General/path.ML";
    3.11  use "General/url.ML";
    3.12  use "General/file.ML";
     4.1 --- a/src/Pure/pure_setup.ML	Tue Jul 12 23:22:22 2011 +0200
     4.2 +++ b/src/Pure/pure_setup.ML	Wed Jul 13 10:57:09 2011 +0200
     4.3 @@ -18,7 +18,6 @@
     4.4  
     4.5  (* ML toplevel pretty printing *)
     4.6  
     4.7 -toplevel_pp ["XML", "tree"] "Pretty.str o XML.string_of";
     4.8  toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
     4.9  toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
    4.10  toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";