author | wenzelm |
Sun, 23 Jun 2013 18:11:38 +0200 | |
changeset 52426 | 81e27230a8b7 |
parent 52425 | de8a85aad216 |
child 62356 | e307a410f46c |
permissions | -rw-r--r-- |
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
43791
diff
changeset
|
1 |
(* Title: Pure/ML/install_pp_polyml.ML |
38327 | 2 |
Author: Makarius |
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
3 |
|
50910 | 4 |
Extra toplevel pretty-printing for Poly/ML. |
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
5 |
*) |
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
6 |
|
41415
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
38327
diff
changeset
|
7 |
PolyML.addPrettyPrinter (fn depth => fn _ => fn str => |
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
38327
diff
changeset
|
8 |
ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str))); |
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
38327
diff
changeset
|
9 |
|
43791 | 10 |
PolyML.addPrettyPrinter (fn depth => fn _ => fn tree => |
11 |
ml_pretty (Pretty.to_ML (XML.pretty depth tree))); |
|
12 |
||
33767 | 13 |
PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => |
14 |
pretty (Synchronized.value var, depth)); |
|
15 |
||
31318 | 16 |
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
|
17 |
(case Future.peek x of |
31318 | 18 |
NONE => PolyML.PrettyString "<future>" |
19 |
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
41415
diff
changeset
|
20 |
| SOME (Exn.Res y) => pretty (y, depth))); |
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
21 |
|
31318 | 22 |
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
|
23 |
(case Lazy.peek x of |
31318 | 24 |
NONE => PolyML.PrettyString "<lazy>" |
25 |
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
41415
diff
changeset
|
26 |
| SOME (Exn.Res y) => pretty (y, depth))); |
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
27 |
|
52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
28 |
|
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
29 |
local |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
30 |
|
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
31 |
open PolyML; |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
32 |
val from_ML = Pretty.from_ML o pretty_ml; |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
33 |
fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt]; |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
34 |
fun prt_apps name = Pretty.enum "," (name ^ " (") ")"; |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
35 |
|
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
36 |
fun prt_term parens dp t = |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
37 |
if dp <= 0 then Pretty.str "..." |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
38 |
else |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
39 |
(case t of |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
40 |
_ $ _ => |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
41 |
op :: (strip_comb t) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
42 |
|> map_index (fn (i, u) => prt_term true (dp - i - 1) u) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
43 |
|> Pretty.separate " $" |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
44 |
|> (if parens then Pretty.enclose "(" ")" else Pretty.block) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
45 |
| Abs (a, T, b) => |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
46 |
prt_apps "Abs" |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
47 |
[from_ML (prettyRepresentation (a, dp - 1)), |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
48 |
from_ML (prettyRepresentation (T, dp - 2)), |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
49 |
prt_term false (dp - 3) b] |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
50 |
| Const a => prt_app "Const" (from_ML (prettyRepresentation (a, dp - 1))) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
51 |
| Free a => prt_app "Free" (from_ML (prettyRepresentation (a, dp - 1))) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
52 |
| Var a => prt_app "Var" (from_ML (prettyRepresentation (a, dp - 1))) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
53 |
| Bound a => prt_app "Bound" (from_ML (prettyRepresentation (a, dp - 1)))); |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
54 |
|
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
55 |
in |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
56 |
|
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
57 |
val _ = |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
58 |
PolyML.addPrettyPrinter (fn depth => fn _ => fn t => |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
59 |
ml_pretty (Pretty.to_ML (prt_term false depth t))); |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
60 |
|
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
61 |
local |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
62 |
|
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
63 |
fun prt_proof parens dp prf = |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
64 |
if dp <= 0 then Pretty.str "..." |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
65 |
else |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
66 |
(case prf of |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
67 |
_ % _ => prt_proofs parens dp prf |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
68 |
| _ %% _ => prt_proofs parens dp prf |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
69 |
| Abst (a, T, b) => |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
70 |
prt_apps "Abst" |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
71 |
[from_ML (prettyRepresentation (a, dp - 1)), |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
72 |
from_ML (prettyRepresentation (T, dp - 2)), |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
73 |
prt_proof false (dp - 3) b] |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
74 |
| AbsP (a, t, b) => |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
75 |
prt_apps "AbsP" |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
76 |
[from_ML (prettyRepresentation (a, dp - 1)), |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
77 |
from_ML (prettyRepresentation (t, dp - 2)), |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
78 |
prt_proof false (dp - 3) b] |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
79 |
| Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
80 |
| MinProof => Pretty.str "MinProof" |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
81 |
| PBound a => prt_app "PBound" (from_ML (prettyRepresentation (a, dp - 1))) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
82 |
| PAxm a => prt_app "PAxm" (from_ML (prettyRepresentation (a, dp - 1))) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
83 |
| OfClass a => prt_app "OfClass" (from_ML (prettyRepresentation (a, dp - 1))) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
84 |
| Oracle a => prt_app "Oracle" (from_ML (prettyRepresentation (a, dp - 1))) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
85 |
| Promise a => prt_app "Promise" (from_ML (prettyRepresentation (a, dp - 1))) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
86 |
| PThm a => prt_app "PThm" (from_ML (prettyRepresentation (a, dp - 1)))) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
87 |
|
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
88 |
and prt_proofs parens dp prf = |
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
|
89 |
let |
52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
90 |
val (head, args) = strip_proof prf []; |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
91 |
val prts = head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - i - 2)) args); |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
92 |
in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
93 |
|
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
94 |
and strip_proof (p % t) res = |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
95 |
strip_proof p |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
96 |
((fn d => [Pretty.str " %", Pretty.brk 1, from_ML (prettyRepresentation (t, d))]) :: res) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
97 |
| strip_proof (p %% q) res = |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
98 |
strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res) |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
99 |
| strip_proof p res = (fn d => prt_proof true d p, res); |
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
|
100 |
|
52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
101 |
in |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
102 |
|
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
103 |
val _ = |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
104 |
PolyML.addPrettyPrinter (fn depth => fn _ => fn prf => |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
105 |
ml_pretty (Pretty.to_ML (prt_proof false depth prf))); |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
106 |
|
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
107 |
end; |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
108 |
|
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
109 |
end; |
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset
|
110 |