92 | convert _ (PrettyBreak (wd, _)) = |
92 | convert _ (PrettyBreak (wd, _)) = |
93 ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2)); |
93 ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2)); |
94 in convert "" end; |
94 in convert "" end; |
95 |
95 |
96 fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) = |
96 fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) = |
97 PrettyBlock (ind, false, |
97 let val context = |
98 [ContextProperty ("begin", bg), ContextProperty ("end", en)], map ml_pretty prts) |
98 (if bg = "" then [] else [ContextProperty ("begin", bg)]) @ |
|
99 (if en = "" then [] else [ContextProperty ("end", en)]) |
|
100 in PrettyBlock (ind, false, context, map ml_pretty prts) end |
99 | ml_pretty (ML_Pretty.String (s, len)) = |
101 | ml_pretty (ML_Pretty.String (s, len)) = |
100 if len = size s then PrettyString s |
102 if len = size s then PrettyString s |
101 else PrettyBlock (0, false, [ContextProperty ("length", Int.toString len)], [PrettyString s]) |
103 else PrettyBlock (0, false, [ContextProperty ("length", Int.toString len)], [PrettyString s]) |
102 | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0) |
104 | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0) |
103 | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0); |
105 | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0); |