src/Pure/PIDE/xml.ML
changeset 62663 bea354f6ff21
parent 61707 d5ddd022a451
child 62819 d3ff367a16a0
--- a/src/Pure/PIDE/xml.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/PIDE/xml.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -170,6 +170,9 @@
 fun pretty depth tree =
   Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
 
+val _ =
+  PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
+
 
 
 (** XML parsing **)