183 |
183 |
184 @{ML_response [display, gray] |
184 @{ML_response [display, gray] |
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 |
189 easy to install your own pretty printer. With the function below we |
189 (version 5.3) it is easy to install your own pretty printer. With the |
190 mimic the behaviour of the usual pretty printer for datatypes (it |
190 function below we mimic the behaviour of the usual pretty printer for |
191 uses pretty-printing functions which will be explained in more detail in |
191 datatypes (it uses pretty-printing functions which will be explained in more |
192 Section~\ref{sec:pretty}). |
192 detail in Section~\ref{sec:pretty}). |
193 *} |
193 *} |
194 |
194 |
195 ML{*fun raw_pp_typ ty = |
195 ML{*local |
196 let |
196 fun pp_pair (x, y) = Pretty.list "(" ")" [x, y] |
197 fun pp_pair (x1, x2) = Pretty.list "(" ")" [x1, x2] |
|
198 fun pp_list xs = Pretty.list "[" "]" xs |
197 fun pp_list xs = Pretty.list "[" "]" xs |
199 fun pp_str s = Pretty.str s |
198 fun pp_str s = Pretty.str s |
200 fun pp_qstr s = Pretty.quote (pp_str s) |
199 fun pp_qstr s = Pretty.quote (pp_str s) |
201 fun pp_int i = pp_str (string_of_int i) |
200 fun pp_int i = pp_str (string_of_int i) |
202 fun pp_sort S = pp_list (map pp_qstr S) |
201 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] |
202 fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args] |
204 in |
203 in |
205 case ty of |
204 fun raw_pp_typ (TVar ((a, i), S)) = |
206 TVar ((a, i), S) => |
|
207 pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S)) |
205 pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S)) |
208 | TFree (a, S) => |
206 | raw_pp_typ (TFree (a, S)) = |
209 pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S)) |
207 pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S)) |
210 | Type (a, tys) => |
208 | raw_pp_typ (Type (a, tys)) = |
211 pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys))) |
209 pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys))) |
212 end*} |
210 end*} |
213 |
211 |
214 text {* |
212 text {* |
215 We can install this pretty printer with the function |
213 We can install this pretty printer with the function |
216 @{ML_ind addPrettyPrinter in PolyML} as follows. |
214 @{ML_ind addPrettyPrinter in PolyML} as follows. |
217 *} |
215 *} |
218 |
216 |
219 ML{*let |
217 ML{*PolyML.addPrettyPrinter |
220 fun pp _ _ = ml_pretty o Pretty.to_ML o raw_pp_typ |
218 (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)*} |
221 in |
|
222 PolyML.addPrettyPrinter pp |
|
223 end*} |
|
224 |
219 |
225 text {* |
220 text {* |
226 Now the type bool is printed out in full detail. |
221 Now the type bool is printed out in full detail. |
227 |
222 |
228 @{ML_response [display,gray] |
223 @{ML_response [display,gray] |