--- 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