author | haftmann |
Mon, 08 Feb 2010 17:12:22 +0100 | |
changeset 35045 | a77d200e6503 |
parent 31313 | 97800f7e80b4 |
permissions | -rw-r--r-- |
31313 | 1 |
(* Title: Pure/ML-Systems/pp_polyml.ML |
30627
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 |
|
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30627
diff
changeset
|
17 |
fun toplevel_pp context (_: string list) pp = |
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30627
diff
changeset
|
18 |
use_text context (1, "pp") false |
31313 | 19 |
("PolyML.install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))"); |
30627
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff
changeset
|
20 |