equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/ml_pretty.ML |
1 (* Title: Pure/ML-Systems/ml_pretty.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Raw datatype for ML pretty printing. |
4 Minimal support for raw ML pretty printing -- for boot-strapping only. |
5 *) |
5 *) |
6 |
6 |
7 structure ML_Pretty = |
7 structure ML_Pretty = |
8 struct |
8 struct |
9 |
9 |
10 datatype pretty = |
10 datatype pretty = |
11 Block of (string * string) * pretty list * int | |
11 Block of (string * string) * pretty list * int | |
12 String of string * int | |
12 String of string * int | |
13 Break of bool * int; |
13 Break of bool * int; |
14 |
14 |
|
15 fun block prts = Block (("", ""), prts, 2); |
|
16 fun str s = String (s, size s); |
|
17 fun brk wd = Break (false, wd); |
|
18 |
|
19 fun pair pretty1 pretty2 ((x, y), depth: int) = |
|
20 block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"]; |
|
21 |
|
22 fun enum sep lpar rpar pretty (args, depth) = |
|
23 let |
|
24 fun elems _ [] = [] |
|
25 | elems 0 _ = [str "..."] |
|
26 | elems d [x] = [pretty (x, d)] |
|
27 | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs; |
|
28 in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end; |
|
29 |
15 end; |
30 end; |
16 |
31 |