--- a/NEWS Sat Oct 05 14:58:36 2024 +0200
+++ b/NEWS Sat Oct 05 15:18:49 2024 +0200
@@ -139,6 +139,8 @@
Note that basic Markup.markup cannot be used for Latex output: proper
Pretty.T operations are required (e.g. Pretty.mark_str).
+* Antiquotation \<^bundle>\<open>name\<close> inlines a formally checked bundle name.
+
*** System ***
--- a/etc/symbols Sat Oct 05 14:58:36 2024 +0200
+++ b/etc/symbols Sat Oct 05 15:18:49 2024 +0200
@@ -443,6 +443,7 @@
\<^action> code: 0x00261b group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
\<^assert>
\<^binding> argument: cartouche
+\<^bundle> argument: cartouche
\<^can> argument: cartouche
\<^class> argument: cartouche
\<^class_syntax> argument: cartouche
--- a/src/Pure/Isar/bundle.ML Sat Oct 05 14:58:36 2024 +0200
+++ b/src/Pure/Isar/bundle.ML Sat Oct 05 15:18:49 2024 +0200
@@ -55,6 +55,11 @@
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_all ctxt);
+val _ = Theory.setup
+ (ML_Antiquotation.inline_embedded \<^binding>\<open>bundle\<close>
+ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
+ ML_Syntax.print_string (check ctxt (name, pos)))));
+
fun check_name ctxt ((b: bool, pos), arg) =
(Context_Position.report ctxt pos Markup.quasi_keyword; (b, check ctxt arg));