src/Pure/ML-Systems/polyml-experimental.ML
changeset 30638 15cc4ad0e6e9
parent 30626 248de8dd839e
child 30673 60568c168040
equal deleted inserted replaced
30637:3e3c2cd88cf1 30638:15cc4ad0e6e9
    70 end;
    70 end;
    71 
    71 
    72 
    72 
    73 (* toplevel pretty printing *)
    73 (* toplevel pretty printing *)
    74 
    74 
       
    75 fun pretty_ml (PrettyBlock (ind, _, _, prts)) = ML_Pretty.Block (("", ""), map pretty_ml prts, ind)
       
    76   | pretty_ml (PrettyString s) = ML_Pretty.String (s, size s)
       
    77   | pretty_ml (PrettyBreak (wd, _)) = ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
       
    78 
    75 fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
    79 fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
    76   | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
    80   | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
    77   | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
    81   | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
    78   | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
    82   | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
    79 
    83