240 (fn {source = src, context = ctxt, ...} => fn dtco => |
240 (fn {source = src, context = ctxt, ...} => fn dtco => |
241 let |
241 let |
242 val thy = ProofContext.theory_of ctxt; |
242 val thy = ProofContext.theory_of ctxt; |
243 val (vs, cos) = the_spec thy dtco; |
243 val (vs, cos) = the_spec thy dtco; |
244 val ty = Type (dtco, map TFree vs); |
244 val ty = Type (dtco, map TFree vs); |
245 fun pretty_typ_bracket (ty as Type (_, _ :: _)) = |
245 val pretty_typ_bracket = |
246 Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty] |
246 Syntax.pretty_typ (Config.put Syntax.pretty_priority (Syntax.max_pri + 1) ctxt); |
247 | pretty_typ_bracket ty = |
|
248 Syntax.pretty_typ ctxt ty; |
|
249 fun pretty_constr (co, tys) = |
247 fun pretty_constr (co, tys) = |
250 (Pretty.block o Pretty.breaks) |
248 Pretty.block (Pretty.breaks |
251 (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) :: |
249 (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) :: |
252 map pretty_typ_bracket tys); |
250 map pretty_typ_bracket tys)); |
253 val pretty_datatype = |
251 val pretty_datatype = |
254 Pretty.block |
252 Pretty.block |
255 (Pretty.command "datatype" :: Pretty.brk 1 :: |
253 (Pretty.command "datatype" :: Pretty.brk 1 :: |
256 Syntax.pretty_typ ctxt ty :: |
254 Syntax.pretty_typ ctxt ty :: |
257 Pretty.str " =" :: Pretty.brk 1 :: |
255 Pretty.str " =" :: Pretty.brk 1 :: |
258 flat (separate [Pretty.brk 1, Pretty.str "| "] |
256 flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_constr) cos))); |
259 (map (single o pretty_constr) cos))); |
|
260 in |
257 in |
261 Thy_Output.output ctxt (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()]) |
258 Thy_Output.output ctxt |
|
259 (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()]) |
262 end); |
260 end); |
263 |
261 |
264 |
262 |
265 |
263 |
266 (** abstract theory extensions relative to a datatype characterisation **) |
264 (** abstract theory extensions relative to a datatype characterisation **) |