author  wenzelm 
Wed, 17 Feb 2016 23:28:58 +0100  
changeset 62356  e307a410f46c 
parent 52426  81e27230a8b7 
child 62387  ad3eb2889f9a 
permissions  rwrr 
47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
43791
diff
changeset

1 
(* Title: Pure/ML/install_pp_polyml.ML 
38327  2 
Author: Makarius 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

3 

62356  4 
ML toplevel prettyprinting for Poly/ML. 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

5 
*) 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

6 

62356  7 
PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T => 
8 
ml_pretty (Pretty.to_ML (Pretty.str "<pretty>"))); 

9 

10 
PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon => 

11 
ml_pretty (Pretty.to_ML (Lexicon.pp_lexicon lexicon))); 

12 

13 
PolyML.addPrettyPrinter (fn _ => fn _ => fn task => 

14 
ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task)))); 

15 

16 
PolyML.addPrettyPrinter (fn _ => fn _ => fn group => 

17 
ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group)))); 

18 

19 
PolyML.addPrettyPrinter (fn _ => fn _ => fn pos => 

20 
ml_pretty (Pretty.to_ML (Pretty.position pos))); 

21 

22 
PolyML.addPrettyPrinter (fn _ => fn _ => fn binding => 

23 
ml_pretty (Pretty.to_ML (Binding.pp binding))); 

24 

25 
PolyML.addPrettyPrinter (fn _ => fn _ => fn th => 

26 
ml_pretty (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th))); 

27 

28 
PolyML.addPrettyPrinter (fn _ => fn _ => fn ct => 

29 
ml_pretty (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct))); 

30 

31 
PolyML.addPrettyPrinter (fn _ => fn _ => fn cT => 

32 
ml_pretty (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT))); 

33 

34 
PolyML.addPrettyPrinter (fn _ => fn _ => fn T => 

35 
ml_pretty (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T))); 

36 

37 
PolyML.addPrettyPrinter (fn _ => fn _ => fn thy => 

38 
ml_pretty (Pretty.to_ML (Context.pretty_thy thy))); 

39 

40 
PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt => 

41 
ml_pretty (Pretty.to_ML (Proof_Display.pp_context ctxt))); 

42 

43 
PolyML.addPrettyPrinter (fn _ => fn _ => fn ast => 

44 
ml_pretty (Pretty.to_ML (Ast.pretty_ast ast))); 

45 

46 
PolyML.addPrettyPrinter (fn _ => fn _ => fn path => 

47 
ml_pretty (Pretty.to_ML (Path.pretty path))); 

48 

49 
PolyML.addPrettyPrinter (fn _ => fn _ => fn digest => 

50 
ml_pretty (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest))))); 

51 

52 
PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state => 

53 
ml_pretty (Pretty.to_ML (Pretty.str "<Proof.state>"))); 

54 

55 
PolyML.addPrettyPrinter (fn _ => fn _ => fn st => 

56 
ml_pretty (Pretty.to_ML (Toplevel.pretty_abstract st))); 

57 

58 
PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism => 

59 
ml_pretty (Pretty.to_ML (Morphism.pretty morphism))); 

60 

41415
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
38327
diff
changeset

61 
PolyML.addPrettyPrinter (fn depth => fn _ => fn str => 
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
38327
diff
changeset

62 
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

63 

43791  64 
PolyML.addPrettyPrinter (fn depth => fn _ => fn tree => 
65 
ml_pretty (Pretty.to_ML (XML.pretty depth tree))); 

66 

33767  67 
PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => 
68 
pretty (Synchronized.value var, depth)); 

69 

31318  70 
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

71 
(case Future.peek x of 
31318  72 
NONE => PolyML.PrettyString "<future>" 
73 
 SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" 

43761
e72ba84ae58f
tuned signature  corresponding to Scala version;
wenzelm
parents:
41415
diff
changeset

74 
 SOME (Exn.Res y) => pretty (y, depth))); 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

75 

31318  76 
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

77 
(case Lazy.peek x of 
31318  78 
NONE => PolyML.PrettyString "<lazy>" 
79 
 SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" 

43761
e72ba84ae58f
tuned signature  corresponding to Scala version;
wenzelm
parents:
41415
diff
changeset

80 
 SOME (Exn.Res y) => pretty (y, depth))); 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

81 

52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

82 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

83 
local 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

84 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

85 
open PolyML; 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

86 
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

87 
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

88 
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

89 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

90 
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

91 
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

92 
else 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

93 
(case t of 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

94 
_ $ _ => 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

95 
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

96 
> 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

97 
> Pretty.separate " $" 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

98 
> (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

99 
 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

100 
prt_apps "Abs" 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

101 
[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

102 
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

103 
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

104 
 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

105 
 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

106 
 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

107 
 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

108 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

109 
in 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

110 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

111 
val _ = 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

112 
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

113 
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

114 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

115 
local 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

116 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

117 
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

118 
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

119 
else 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

120 
(case prf of 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

121 
_ % _ => 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

122 
 _ %% _ => 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

123 
 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

124 
prt_apps "Abst" 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

125 
[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

126 
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

127 
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

128 
 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

129 
prt_apps "AbsP" 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

130 
[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

131 
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

132 
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

133 
 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

134 
 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

135 
 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

136 
 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

137 
 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

138 
 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

139 
 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

140 
 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

141 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

142 
and prt_proofs parens dp prf = 
33545
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

143 
let 
52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

144 
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

145 
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

146 
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

147 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

148 
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

149 
strip_proof p 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

150 
((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

151 
 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

152 
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

153 
 strip_proof p res = (fn d => prt_proof true d p, res); 
33545
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

154 

52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

155 
in 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

156 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

157 
val _ = 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

158 
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

159 
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

160 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

161 
end; 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

162 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

163 
end; 