--- a/src/Doc/Isar_Ref/Document_Preparation.thy Wed Aug 04 22:20:47 2021 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Thu Aug 05 07:12:49 2021 +0000
@@ -95,6 +95,7 @@
@{antiquotation_def type} & : & \<open>antiquotation\<close> \\
@{antiquotation_def class} & : & \<open>antiquotation\<close> \\
@{antiquotation_def locale} & : & \<open>antiquotation\<close> \\
+ @{antiquotation_def bundle} & : & \<open>antiquotation\<close> \\
@{antiquotation_def "text"} & : & \<open>antiquotation\<close> \\
@{antiquotation_def goals} & : & \<open>antiquotation\<close> \\
@{antiquotation_def subgoals} & : & \<open>antiquotation\<close> \\
@@ -195,6 +196,7 @@
@@{antiquotation type} options @{syntax embedded} |
@@{antiquotation class} options @{syntax embedded} |
@@{antiquotation locale} options @{syntax embedded} |
+ @@{antiquotation bundle} options @{syntax embedded} |
(@@{antiquotation command} | @@{antiquotation method} | @@{antiquotation attribute})
options @{syntax name}
;
@@ -272,6 +274,8 @@
\<^descr> \<open>@{locale c}\<close> prints a locale \<open>c\<close>.
+ \<^descr> \<open>@{bundle c}\<close> prints a bundle \<open>c\<close>.
+
\<^descr> \<open>@{command name}\<close>, \<open>@{method name}\<close>, \<open>@{attribute name}\<close> print checked
entities of the Isar language.
--- a/src/Pure/Isar/bundle.ML Wed Aug 04 22:20:47 2021 +0200
+++ b/src/Pure/Isar/bundle.ML Thu Aug 05 07:12:49 2021 +0000
@@ -10,6 +10,7 @@
val check: Proof.context -> xstring * Position.T -> string
val get: Proof.context -> name -> Attrib.thms
val read: Proof.context -> xstring * Position.T -> Attrib.thms
+ val extern: Proof.context -> string -> xstring
val print_bundles: bool -> Proof.context -> unit
val bundle: binding * Attrib.thms ->
(binding * typ option * mixfix) list -> local_theory -> local_theory
@@ -54,6 +55,8 @@
fun read ctxt = get ctxt o check ctxt;
+fun extern ctxt = Name_Space.extern ctxt (Name_Space.space_of_table (get_all ctxt));
+
fun define_bundle (b, bundle) context =
let
val bundle' = Attrib.trim_context_thms bundle;
--- a/src/Pure/Thy/document_antiquotations.ML Wed Aug 04 22:20:47 2021 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Thu Aug 05 07:12:49 2021 +0000
@@ -50,6 +50,9 @@
let val thy = Proof_Context.theory_of ctxt
in Pretty.str (Locale.extern thy (Locale.check thy (name, pos))) end;
+fun pretty_bundle ctxt (name, pos) =
+ Pretty.str (Bundle.extern ctxt (Bundle.check ctxt (name, pos)));
+
fun pretty_class ctxt s =
Pretty.str (Proof_Context.extern_class ctxt (Proof_Context.read_class ctxt s));
@@ -78,6 +81,7 @@
basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #>
basic_entity \<^binding>\<open>locale\<close> (Scan.lift Args.embedded_position) pretty_locale #>
+ basic_entity \<^binding>\<open>bundle\<close> (Scan.lift Args.embedded_position) pretty_bundle #>
basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #>
basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded_inner_syntax) pretty_type #>
basic_entity \<^binding>\<open>theory\<close> (Scan.lift Args.embedded_position) pretty_theory #>