equal
deleted
inserted
replaced
168 val output = Buffer.output o buffer_of ~1; |
168 val output = Buffer.output o buffer_of ~1; |
169 |
169 |
170 fun pretty depth tree = |
170 fun pretty depth tree = |
171 Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree)); |
171 Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree)); |
172 |
172 |
|
173 val _ = |
|
174 PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth)); |
|
175 |
173 |
176 |
174 |
177 |
175 (** XML parsing **) |
178 (** XML parsing **) |
176 |
179 |
177 local |
180 local |