| changeset 41415 | 23533273220a |
| parent 38327 | d6afb77b0f6d |
| child 43761 | e72ba84ae58f |
--- a/src/Pure/ML/install_pp_polyml-5.3.ML Wed Dec 29 18:18:42 2010 +0100 +++ b/src/Pure/ML/install_pp_polyml-5.3.ML Wed Dec 29 20:41:33 2010 +0100 @@ -4,6 +4,9 @@ Extra toplevel pretty-printing for Poly/ML 5.3.0. *) +PolyML.addPrettyPrinter (fn depth => fn _ => fn str => + ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str))); + PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => pretty (Synchronized.value var, depth));