author | wenzelm |
Sat, 21 Nov 2009 17:01:44 +0100 | |
changeset 33834 | 7c06e19f717c |
parent 33767 | f962c761a38f |
permissions | -rw-r--r-- |
31433 | 1 |
(* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML |
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
2 |
|
33538
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
31433
diff
changeset
|
3 |
Extra toplevel pretty-printing for Poly/ML 5.3.0. |
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
4 |
*) |
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
5 |
|
33767 | 6 |
PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => |
7 |
pretty (Synchronized.value var, depth)); |
|
8 |
||
31318 | 9 |
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
10 |
(case Future.peek x of |
31318 | 11 |
NONE => PolyML.PrettyString "<future>" |
12 |
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
|
30714
88bc86d7dec3
simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally;
wenzelm
parents:
30633
diff
changeset
|
13 |
| SOME (Exn.Result y) => pretty (y, depth))); |
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
14 |
|
31318 | 15 |
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
16 |
(case Lazy.peek x of |
31318 | 17 |
NONE => PolyML.PrettyString "<lazy>" |
18 |
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
|
30714
88bc86d7dec3
simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally;
wenzelm
parents:
30633
diff
changeset
|
19 |
| SOME (Exn.Result y) => pretty (y, depth))); |
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
20 |
|
33545
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
21 |
PolyML.addPrettyPrinter (fn depth => fn _ => fn tm => |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
22 |
let |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
23 |
open PolyML; |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
24 |
val from_ML = Pretty.from_ML o pretty_ml; |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
25 |
fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt]; |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
26 |
fun prt_apps name = Pretty.enum "," (name ^ " (") ")"; |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
27 |
fun prt_term parens dp (t as _ $ _) = |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
28 |
op :: (strip_comb t) |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
29 |
|> map_index (fn (i, u) => prt_term true (dp - i - 1) u) |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
30 |
|> Pretty.separate " $" |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
31 |
|> (if parens then Pretty.enclose "(" ")" else Pretty.block) |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
32 |
| prt_term _ dp (Abs (x, T, body)) = |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
33 |
prt_apps "Abs" |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
34 |
[from_ML (prettyRepresentation (x, dp - 1)), |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
35 |
from_ML (prettyRepresentation (T, dp - 2)), |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
36 |
prt_term false (dp - 3) body] |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
37 |
| prt_term _ dp (Const const) = |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
38 |
prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1))) |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
39 |
| prt_term _ dp (Free free) = |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
40 |
prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1))) |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
41 |
| prt_term _ dp (Var var) = |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
42 |
prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1))) |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
43 |
| prt_term _ dp (Bound i) = |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
44 |
prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1))); |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
45 |
in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end); |
d8903f0002e5
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset
|
46 |