author | wenzelm |
Sat, 21 Mar 2009 20:00:23 +0100 | |
changeset 30627 | fb9e73c01603 |
child 30672 | beaadd5af500 |
permissions | -rw-r--r-- |
30627
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/polyml_pp.ML |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
2 |
|
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
3 |
Toplevel pretty printing for Poly/ML before 5.3. |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
4 |
*) |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
5 |
|
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
6 |
fun ml_pprint (print, begin_blk, brk, end_blk) = |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
7 |
let |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
8 |
fun str "" = () |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
9 |
| str s = print s; |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
10 |
fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) = |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
11 |
(str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en) |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
12 |
| pprint (ML_Pretty.String (s, _)) = str s |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
13 |
| pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0) |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
14 |
| pprint (ML_Pretty.Break (true, _)) = brk (99999, 0); |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
15 |
in pprint end; |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
16 |
|
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
17 |
fun toplevel_pp tune str_of_pos output (_: string list) pp = |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
18 |
use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
19 |
("install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))"); |
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
20 |