# HG changeset patch # User wenzelm # Date 1575629009 -3600 # Node ID 6e0ff949073e6a1d62628da044b80360e4716a89 # Parent 30db0523f9b011ede80ebeb0b0f374ba454460c1 clarified modules; diff -r 30db0523f9b0 -r 6e0ff949073e src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Dec 06 11:36:20 2019 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Dec 06 11:43:29 2019 +0100 @@ -981,47 +981,4 @@ (((pre_bnfs, absT_infos), comp_cache'), res) end; - -(** document antiquotations **) - -local - -fun antiquote_setup binding co = - Thy_Output.antiquotation_pretty_source_embedded binding - ((Scan.ahead (Scan.lift Parse.not_eof) >> Token.pos_of) -- - Args.type_name {proper = true, strict = true}) - (fn ctxt => fn (pos, type_name) => - let - fun err () = - error ("Bad " ^ Binding.name_of binding ^ ": " ^ quote type_name ^ Position.here pos); - in - (case Ctr_Sugar.ctr_sugar_of ctxt type_name of - NONE => err () - | SOME {kind, T = T0, ctrs = ctrs0, ...} => - let - val _ = if co = (kind = Codatatype) then () else err (); - - val T = Logic.unvarifyT_global T0; - val ctrs = map Logic.unvarify_global 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)))); - in - 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))) - end) - end); - -in - -val _ = - Theory.setup - (antiquote_setup \<^binding>\datatype\ false #> - antiquote_setup \<^binding>\codatatype\ true); - end; - -end; diff -r 30db0523f9b0 -r 6e0ff949073e src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Dec 06 11:36:20 2019 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Dec 06 11:43:29 2019 +0100 @@ -1187,4 +1187,48 @@ -- parse_sel_default_eqs >> free_constructors_cmd Unknown); + + +(** document antiquotations **) + +local + +fun antiquote_setup binding co = + Thy_Output.antiquotation_pretty_source_embedded binding + ((Scan.ahead (Scan.lift Parse.not_eof) >> Token.pos_of) -- + Args.type_name {proper = true, strict = true}) + (fn ctxt => fn (pos, type_name) => + let + fun err () = + error ("Bad " ^ Binding.name_of binding ^ ": " ^ quote type_name ^ Position.here pos); + in + (case ctr_sugar_of ctxt type_name of + NONE => err () + | SOME {kind, T = T0, ctrs = ctrs0, ...} => + let + val _ = if co = (kind = Codatatype) then () else err (); + + val T = Logic.unvarifyT_global T0; + val ctrs = map Logic.unvarify_global 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)))); + in + 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))) + end) + end); + +in + +val _ = + Theory.setup + (antiquote_setup \<^binding>\datatype\ false #> + antiquote_setup \<^binding>\codatatype\ true); + end; + +end;