src/Pure/ML/ml_syntax.ML
changeset 62663 bea354f6ff21
parent 62528 c8c532b22947
child 62819 d3ff367a16a0
--- a/src/Pure/ML/ml_syntax.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -123,4 +123,8 @@
       else take (Int.max (max_len, 0)) body @ ["..."];
   in Pretty.str (quote (implode (map print_char body'))) end;
 
+val _ =
+  PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
+    Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str));
+
 end;