73 end; |
73 end; |
74 |
74 |
75 |
75 |
76 (* toplevel pretty printing *) |
76 (* toplevel pretty printing *) |
77 |
77 |
78 fun pretty_ml (PrettyBlock (ind, _, _, prts)) = ML_Pretty.Block (("", ""), map pretty_ml prts, ind) |
78 val pretty_ml = |
79 | pretty_ml (PrettyString s) = ML_Pretty.String (s, size s) |
79 let |
80 | pretty_ml (PrettyBreak (wd, _)) = ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2)); |
80 fun convert len (PrettyBlock (ind, _, context, prts)) = |
|
81 let |
|
82 fun property name default = |
|
83 (case List.find (fn ContextProperty (a, _) => name = a | _ => false) context of |
|
84 SOME (ContextProperty (_, b)) => b |
|
85 | NONE => default); |
|
86 val bg = property "begin" ""; |
|
87 val en = property "end" ""; |
|
88 val len' = property "length" len; |
|
89 in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end |
|
90 | convert len (PrettyString s) = |
|
91 ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s) |
|
92 | convert _ (PrettyBreak (wd, _)) = |
|
93 ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2)); |
|
94 in convert "" end; |
81 |
95 |
82 fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts) |
96 fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) = |
83 | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s |
97 PrettyBlock (ind, false, |
|
98 [ContextProperty ("begin", bg), ContextProperty ("end", en)], map ml_pretty prts) |
|
99 | ml_pretty (ML_Pretty.String (s, len)) = |
|
100 if len = size s then PrettyString s |
|
101 else PrettyBlock (0, false, [ContextProperty ("length", Int.toString len)], [PrettyString s]) |
84 | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0) |
102 | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0) |
85 | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0); |
103 | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0); |
86 |
104 |
87 fun toplevel_pp context (_: string list) pp = |
105 fun toplevel_pp context (_: string list) pp = |
88 use_text context (1, "pp") false |
106 use_text context (1, "pp") false |