1 (* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML |
|
2 |
|
3 Extra toplevel pretty-printing for Poly/ML 5.3.0. |
|
4 *) |
|
5 |
|
6 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => |
|
7 pretty (Synchronized.value var, depth)); |
|
8 |
|
9 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |
|
10 (case Future.peek x of |
|
11 NONE => PolyML.PrettyString "<future>" |
|
12 | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
|
13 | SOME (Exn.Result y) => pretty (y, depth))); |
|
14 |
|
15 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |
|
16 (case Lazy.peek x of |
|
17 NONE => PolyML.PrettyString "<lazy>" |
|
18 | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
|
19 | SOME (Exn.Result y) => pretty (y, depth))); |
|
20 |
|
21 PolyML.addPrettyPrinter (fn depth => fn _ => fn tm => |
|
22 let |
|
23 open PolyML; |
|
24 val from_ML = Pretty.from_ML o pretty_ml; |
|
25 fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt]; |
|
26 fun prt_apps name = Pretty.enum "," (name ^ " (") ")"; |
|
27 fun prt_term parens dp (t as _ $ _) = |
|
28 op :: (strip_comb t) |
|
29 |> map_index (fn (i, u) => prt_term true (dp - i - 1) u) |
|
30 |> Pretty.separate " $" |
|
31 |> (if parens then Pretty.enclose "(" ")" else Pretty.block) |
|
32 | prt_term _ dp (Abs (x, T, body)) = |
|
33 prt_apps "Abs" |
|
34 [from_ML (prettyRepresentation (x, dp - 1)), |
|
35 from_ML (prettyRepresentation (T, dp - 2)), |
|
36 prt_term false (dp - 3) body] |
|
37 | prt_term _ dp (Const const) = |
|
38 prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1))) |
|
39 | prt_term _ dp (Free free) = |
|
40 prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1))) |
|
41 | prt_term _ dp (Var var) = |
|
42 prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1))) |
|
43 | prt_term _ dp (Bound i) = |
|
44 prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1))); |
|
45 in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end); |
|
46 |
|