added pretty_ml;
authorwenzelm
Sun, 22 Mar 2009 19:10:59 +0100
changeset 30638 15cc4ad0e6e9
parent 30637 3e3c2cd88cf1
child 30639 fe40d740d7c1
added pretty_ml;
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)