# HG changeset patch
# User wenzelm
# Date 1237745459 -3600
# Node ID 15cc4ad0e6e9dd43eebc8cf58c42ff37326c280e
# Parent  3e3c2cd88cf1fa18875bfe8056cd4bddb99d8280
added pretty_ml;

diff -r 3e3c2cd88cf1 -r 15cc4ad0e6e9 src/Pure/ML-Systems/polyml-experimental.ML
--- a/src/Pure/ML-Systems/polyml-experimental.ML	Sun Mar 22 19:10:59 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-experimental.ML	Sun Mar 22 19:10:59 2009 +0100
@@ -72,6 +72,10 @@
 
 (* toplevel pretty printing *)
 
+fun pretty_ml (PrettyBlock (ind, _, _, prts)) = ML_Pretty.Block (("", ""), map pretty_ml prts, ind)
+  | pretty_ml (PrettyString s) = ML_Pretty.String (s, size s)
+  | pretty_ml (PrettyBreak (wd, _)) = ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
+
 fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
   | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
   | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)