# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 08c0f0d4b9f4483d675ad932376ab7c06e121182
# Parent  9dfe8506c04ddfffb077fda303d96db016ebe63a
generalized 'datatype' LaTeX antiquotation and added 'codatatype'

diff -r 9dfe8506c04d -r 08c0f0d4b9f4 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -2,6 +2,7 @@
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Martin Desharnais, TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
     Copyright   2012, 2013, 2014
 
 Shared library for the datatype and codatatype constructions.
@@ -187,6 +188,7 @@
       BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) ->
     binding list -> (string * sort) list -> (string * sort) list -> ((string * sort) * typ) list ->
     local_theory -> (BNF_Def.bnf list * BNF_Comp.absT_info list) * 'a
+  val fp_antiquote_setup: binding -> theory -> theory
 end;
 
 structure BNF_FP_Util : BNF_FP_UTIL =
@@ -630,4 +632,29 @@
     timer; ((pre_bnfs, absT_infos), res)
   end;
 
+fun fp_antiquote_setup binding =
+  Thy_Output.antiquotation binding (Args.type_name {proper = true, strict = true})
+    (fn {source = src, context = ctxt, ...} => fn fcT_name =>
+       (case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of
+         NONE => error ("Not a known freely generated type name: " ^ quote fcT_name)
+       | SOME {T = T0, ctrs = ctrs0, ...} =>
+         let
+           val freezeT = Term.map_atyps (fn TVar ((s, _), S) => TFree (s, S) | T => T);
+
+           val T = freezeT T0;
+           val ctrs = map (Term.map_types freezeT) ctrs0;
+
+           val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
+           fun pretty_ctr ctr =
+             Pretty.block (Pretty.breaks (Syntax.pretty_term ctxt ctr ::
+               map pretty_typ_bracket (binder_types (fastype_of ctr))));
+           val pretty_co_datatype =
+             Pretty.block (Pretty.keyword1 (Binding.name_of binding) :: Pretty.brk 1 ::
+               Syntax.pretty_typ ctxt T :: Pretty.str " =" :: Pretty.brk 1 ::
+               flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_ctr) ctrs)));
+         in
+           Thy_Output.output ctxt
+             (Thy_Output.maybe_pretty_source (K (K pretty_co_datatype)) ctxt src [()])
+         end));
+
 end;
diff -r 9dfe8506c04d -r 08c0f0d4b9f4 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -2530,4 +2530,6 @@
   Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes"
     (parse_co_datatype_cmd Greatest_FP construct_gfp);
 
+val _ = Theory.setup (fp_antiquote_setup @{binding codatatype});
+
 end;
diff -r 9dfe8506c04d -r 08c0f0d4b9f4 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -1817,4 +1817,6 @@
   Outer_Syntax.local_theory @{command_spec "datatype_new"} "define inductive datatypes"
     (parse_co_datatype_cmd Least_FP construct_lfp);
 
+val _ = Theory.setup (fp_antiquote_setup @{binding datatype});
+
 end;
diff -r 9dfe8506c04d -r 08c0f0d4b9f4 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -1088,6 +1088,6 @@
        -- parse_sel_default_eqs
      >> free_constructors_cmd);
 
-val _ = Context.>> (Context.map_theory Ctr_Sugar_Interpretation.init);
+val _ = Theory.setup Ctr_Sugar_Interpretation.init;
 
 end;
diff -r 9dfe8506c04d -r 08c0f0d4b9f4 src/HOL/Tools/Old_Datatype/old_datatype_data.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -235,33 +235,6 @@
 
 
 
-(** document antiquotation **)
-
-val antiq_setup =
-  Thy_Output.antiquotation @{binding datatype} (Args.type_name {proper = true, strict = true})
-    (fn {source = src, context = ctxt, ...} => fn dtco =>
-      let
-        val thy = Proof_Context.theory_of ctxt;
-        val (vs, cos) = the_spec thy dtco;
-        val ty = Type (dtco, map TFree vs);
-        val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
-        fun pretty_constr (co, tys) =
-          Pretty.block (Pretty.breaks
-            (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
-              map pretty_typ_bracket tys));
-        val pretty_datatype =
-          Pretty.block
-           (Pretty.keyword1 "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
-        Thy_Output.output ctxt
-          (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()])
-      end);
-
-
-
 (** abstract theory extensions relative to a datatype characterisation **)
 
 structure Datatype_Interpretation = Interpretation
@@ -284,7 +257,7 @@
 
 (** setup theory **)
 
-val _ = Theory.setup (antiq_setup #> Datatype_Interpretation.init);
+val _ = Theory.setup Datatype_Interpretation.init;
 
 open Old_Datatype_Aux;