# HG changeset patch # User haftmann # Date 1203678114 -3600 # Node ID 91e0999b075fc47c7bb30dae12bfbff78ae25777 # Parent 06eacfd8dd9f4b693246c77d842ccfdfbf4e3c52 added first version of datatype antiquotation diff -r 06eacfd8dd9f -r 91e0999b075f src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Fri Feb 22 12:01:52 2008 +0100 +++ b/src/HOL/Tools/datatype_package.ML Fri Feb 22 12:01:54 2008 +0100 @@ -886,6 +886,52 @@ val add_datatype = gen_add_datatype read_typ true; +(** a datatype antiquotation **) + +local + +val sym_datatype = Pretty.str "\\isacommand{datatype}"; +val sym_binder = Pretty.str "{\\isacharequal}"; +val sym_of = Pretty.str "of"; +val sym_sep = Pretty.str "{\\isacharbar}"; + +in + +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, []) = + Syntax.pretty_term ctxt (Const (co, ty)) + | pretty_constr (co, [ty']) = + (Pretty.block o Pretty.breaks) + [Syntax.pretty_term ctxt (Const (co, ty' --> ty)), + sym_of, Syntax.pretty_typ ctxt ty'] + | pretty_constr (co, tys) = + (Pretty.block o Pretty.breaks) + (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) :: + sym_of :: map pretty_typ_br tys); + in (Pretty.block o Pretty.breaks) ( + sym_datatype + :: Syntax.pretty_typ ctxt ty + :: sym_binder + :: separate sym_sep (map pretty_constr cos) + ) end + +end; (** package setup **) @@ -933,6 +979,10 @@ OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl (rep_datatype_decl >> (Toplevel.theory o mk_rep_datatype)); +val _ = + ThyOutput.add_commands [("datatype", + ThyOutput.args args_datatype (ThyOutput.output pretty_datatype))]; + end;