| author | blanchet |
| Wed, 02 Jun 2010 15:18:48 +0200 | |
| changeset 37321 | 9d7cfae95b30 |
| 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 |