# HG changeset patch
# User wenzelm
# Date 1621511805 -7200
# Node ID d4202c13bfba26e6397e3256241aae7e47fae68b
# Parent  eeb076fc569f7b91c9bcdd98b6f0bd545f4ecf05
tuned;

diff -r eeb076fc569f -r d4202c13bfba src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Thu May 20 13:50:20 2021 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Thu May 20 13:56:45 2021 +0200
@@ -127,11 +127,11 @@
       (fn _ => fn () => Latex.string "\\bigskip"));
 
 
-(* control style *)
+(* nested document text *)
 
 local
 
-fun control_antiquotation name s1 s2 =
+fun nested_antiquotation name s1 s2 =
   Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input)
     (fn ctxt => fn txt =>
       (Context_Position.reports ctxt (Thy_Output.document_reports txt);
@@ -141,9 +141,9 @@
 
 val _ =
   Theory.setup
-   (control_antiquotation \<^binding>\<open>footnote\<close> "\\footnote{" "}" #>
-    control_antiquotation \<^binding>\<open>emph\<close> "\\emph{" "}" #>
-    control_antiquotation \<^binding>\<open>bold\<close> "\\textbf{" "}");
+   (nested_antiquotation \<^binding>\<open>footnote\<close> "\\footnote{" "}" #>
+    nested_antiquotation \<^binding>\<open>emph\<close> "\\emph{" "}" #>
+    nested_antiquotation \<^binding>\<open>bold\<close> "\\textbf{" "}");
 
 end;
 
@@ -203,8 +203,6 @@
 end;
 
 
-
-
 (* goal state *)
 
 local