equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/pp_polyml.ML |
|
2 |
|
3 Toplevel pretty printing for Poly/ML before 5.3. |
|
4 *) |
|
5 |
|
6 fun ml_pprint (print, begin_blk, brk, end_blk) = |
|
7 let |
|
8 fun str "" = () |
|
9 | str s = print s; |
|
10 fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) = |
|
11 (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en) |
|
12 | pprint (ML_Pretty.String (s, _)) = str s |
|
13 | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0) |
|
14 | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0); |
|
15 in pprint end; |
|
16 |
|
17 fun toplevel_pp context (_: string list) pp = |
|
18 use_text context (1, "pp") false |
|
19 ("PolyML.install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))"); |
|
20 |
|