# HG changeset patch
# User haftmann
# Date 1628147569 0
# Node ID 7d3e818fe21f3d318697e0160a33cf19ec2f5ded
# Parent  bc03b0b82fe6044679baa4a82997e390ecdd3650
antiquotation for bundles

diff -r bc03b0b82fe6 -r 7d3e818fe21f src/Doc/Isar_Ref/Document_Preparation.thy
--- 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.
 
diff -r bc03b0b82fe6 -r 7d3e818fe21f src/Pure/Isar/bundle.ML
--- 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;
diff -r bc03b0b82fe6 -r 7d3e818fe21f src/Pure/Thy/document_antiquotations.ML
--- 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 #>