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