185 "@{typ \"bool\"}" |
185 "@{typ \"bool\"}" |
186 "bool"} |
186 "bool"} |
187 |
187 |
188 that is the pretty printed version of @{text "bool"}. However, in PolyML it is |
188 that is the pretty printed version of @{text "bool"}. However, in PolyML it is |
189 easy to install your own pretty printer. With the function below we |
189 easy to install your own pretty printer. With the function below we |
190 mimic the behaviour of the usual pretty printer for |
190 mimic the behaviour of the usual pretty printer for datatypes (it |
191 datatypes.\footnote{Thanks to David Matthews for providing this |
191 uses pretty-printing functions which will be explained in more detail in |
192 code.} |
192 Section~\ref{sec:pretty}). |
193 *} |
193 *} |
194 |
194 |
195 ML{*fun typ_raw_pretty_printer depth _ ty = |
195 ML{*fun raw_pp_typ ty = |
196 let |
196 let |
197 fun cond str a = |
197 fun pp_pair (x1, x2) = Pretty.list "(" ")" [x1, x2] |
198 if depth <= 0 |
198 fun pp_list xs = Pretty.list "[" "]" xs |
199 then PolyML.PrettyString "..." |
199 fun pp_str s = Pretty.str s |
200 else PolyML.PrettyBlock(1, false, [], |
200 fun pp_qstr s = Pretty.quote (pp_str s) |
201 [PolyML.PrettyString str, PolyML.PrettyBreak(1, 0), a]) |
201 fun pp_int i = pp_str (string_of_int i) |
202 in |
202 fun pp_sort S = pp_list (map pp_qstr S) |
|
203 fun pp_constr s xs = Pretty.block [pp_str s, Pretty.brk 1, xs] |
|
204 in |
203 case ty of |
205 case ty of |
204 Type a => cond "Type" (PolyML.prettyRepresentation(a, depth - 1)) |
206 TVar ((a, i), S) => |
205 | TFree a => cond "TFree" (PolyML.prettyRepresentation(a, depth - 1)) |
207 pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S)) |
206 | TVar a => cond "TVar" (PolyML.prettyRepresentation(a, depth - 1)) |
208 | TFree (a, S) => |
|
209 pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S)) |
|
210 | Type (a, tys) => |
|
211 pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys))) |
207 end*} |
212 end*} |
208 |
213 |
209 text {* |
214 text {* |
210 We can install this pretty printer with the function |
215 We can install this pretty printer with the function |
211 @{ML_ind addPrettyPrinter in PolyML} as follows. |
216 @{ML_ind addPrettyPrinter in PolyML} as follows. |
212 *} |
217 *} |
213 |
218 |
214 ML{*PolyML.addPrettyPrinter typ_raw_pretty_printer*} |
219 ML{*let |
215 |
220 fun pp _ _ = ml_pretty o Pretty.to_ML o raw_pp_typ |
216 (* |
221 in |
217 classes s |
222 PolyML.addPrettyPrinter pp |
218 |
223 end*} |
219 ML {* @{typ "bool \<Rightarrow> ('a::s)"} *} |
|
220 |
|
221 ML {* |
|
222 fun test ty = |
|
223 case ty of |
|
224 TVar ((v, n), s) => Pretty.block [Pretty.str "TVar "] |
|
225 | TFree (x, s) => Pretty.block [Pretty.str "TFree "] |
|
226 | Type (s, tys) => Pretty.block [Pretty.str "Type "] |
|
227 *} |
|
228 |
|
229 ML {* toplevel_pp ["typ"] "test" *} |
|
230 *) |
|
231 |
224 |
232 text {* |
225 text {* |
233 Now the type bool is printed out in full detail. |
226 Now the type bool is printed out in full detail. |
234 |
227 |
235 @{ML_response [display,gray] |
228 @{ML_response [display,gray] |
255 |
248 |
256 We can restore the usual behaviour of Isabelle's pretty printer |
249 We can restore the usual behaviour of Isabelle's pretty printer |
257 with the code |
250 with the code |
258 *} |
251 *} |
259 |
252 |
260 ML{*fun stnd_pretty_printer _ _ = |
253 ML{*let |
261 ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy; |
254 fun pp _ _ = ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy |
262 |
255 in |
263 PolyML.addPrettyPrinter stnd_pretty_printer*} |
256 PolyML.addPrettyPrinter pp |
|
257 end*} |
264 |
258 |
265 text {* |
259 text {* |
266 After that the types for booleans, lists and so on are printed out again |
260 After that the types for booleans, lists and so on are printed out again |
267 the standard Isabelle way. |
261 the standard Isabelle way. |
268 |
262 |