# HG changeset patch # User wenzelm # Date 1236617667 -3600 # Node ID d930432adb13ddcf62a6813cb94ad686ae5e07a1 # Parent ad591ee76c78160ab0e5fdd7df0466c42f321d5e adapted to simplified ThyOutput.antiquotation interface; diff -r ad591ee76c78 -r d930432adb13 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Mon Mar 09 17:53:53 2009 +0100 +++ b/src/HOL/Tools/datatype_package.ML Mon Mar 09 17:54:27 2009 +0100 @@ -628,38 +628,6 @@ val add_datatype_cmd = gen_add_datatype read_typ true; -(** a datatype antiquotation **) - -fun args_datatype (ctxt, args) = - let - val (tyco, (ctxt', args')) = Args.tyname (ctxt, args); - val thy = Context.theory_of ctxt'; - val spec = the_datatype_spec thy tyco; - in ((tyco, spec), (ctxt', args')) end; - -fun pretty_datatype ctxt (dtco, (vs, cos)) = - let - val ty = Type (dtco, map TFree vs); - fun pretty_typ_br ty = - let - val p = Syntax.pretty_typ ctxt ty; - val s = explode (Pretty.str_of p); - in if member (op =) s " " then Pretty.enclose "(" ")" [p] - else p - end; - fun pretty_constr (co, tys) = - (Pretty.block o Pretty.breaks) - (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) :: - map pretty_typ_br tys); - in - Pretty.block - (Pretty.command "datatype" :: Pretty.brk 1 :: - Syntax.pretty_typ ctxt ty :: - Pretty.str " =" :: Pretty.brk 1 :: - flat (separate [Pretty.brk 1, Pretty.str "| "] - (map (single o pretty_constr) cos))) - end - (** package setup **) @@ -698,11 +666,34 @@ >> (fn (alt_names, ts) => Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts))); -val _ = - ThyOutput.add_commands [("datatype", - ThyOutput.args args_datatype (ThyOutput.output pretty_datatype))]; +end; + + +(* document antiquotation *) + +val _ = ThyOutput.antiquotation "datatype" Args.tyname + (fn {source = src, context = ctxt, ...} => fn dtco => + let + val thy = ProofContext.theory_of ctxt; + val (vs, cos) = the_datatype_spec thy dtco; + val ty = Type (dtco, map TFree vs); + fun pretty_typ_br ty = + let + val p = Syntax.pretty_typ ctxt ty; + val s = explode (Pretty.str_of p); (* FIXME do not inspect pretty output! *) + in if member (op =) s " " then Pretty.enclose "(" ")" [p] else p end; + fun pretty_constr (co, tys) = + (Pretty.block o Pretty.breaks) + (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) :: + map pretty_typ_br tys); + val pretty_datatype = + Pretty.block + (Pretty.command "datatype" :: Pretty.brk 1 :: + Syntax.pretty_typ ctxt ty :: + Pretty.str " =" :: Pretty.brk 1 :: + flat (separate [Pretty.brk 1, Pretty.str "| "] + (map (single o pretty_constr) cos))); + in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end); end; -end; -