src/Pure/ML-Systems/polyml-experimental.ML
changeset 30642 15cc4ad0e6e9
parent 30629 248de8dd839e
child 30688 60568c168040
     1.1 --- a/src/Pure/ML-Systems/polyml-experimental.ML	Sun Mar 22 19:10:59 2009 +0100
     1.2 +++ b/src/Pure/ML-Systems/polyml-experimental.ML	Sun Mar 22 19:10:59 2009 +0100
     1.3 @@ -72,6 +72,10 @@
     1.4  
     1.5  (* toplevel pretty printing *)
     1.6  
     1.7 +fun pretty_ml (PrettyBlock (ind, _, _, prts)) = ML_Pretty.Block (("", ""), map pretty_ml prts, ind)
     1.8 +  | pretty_ml (PrettyString s) = ML_Pretty.String (s, size s)
     1.9 +  | pretty_ml (PrettyBreak (wd, _)) = ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
    1.10 +
    1.11  fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
    1.12    | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
    1.13    | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)