# HG changeset patch
# User wenzelm
# Date 1728134329 -7200
# Node ID 0c898f7d9b150b86c3abc5cb704ef8078e7e5d44
# Parent  0fb1e2dd412211b9bce3222a7f255a4ca0707cb4
ML antiquotation for formally-checked bundle names;

diff -r 0fb1e2dd4122 -r 0c898f7d9b15 NEWS
--- 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 ***
 
diff -r 0fb1e2dd4122 -r 0c898f7d9b15 etc/symbols
--- 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
diff -r 0fb1e2dd4122 -r 0c898f7d9b15 src/Pure/Isar/bundle.ML
--- 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));