src/Pure/Thy/document_antiquotations.ML

       (fn _ => fn () => Latex.string "\\medskip") #>
     Thy_Output.antiquotation_raw \<^binding>\<open>bigskip\<close> (Scan.succeed ())
       (fn _ => fn () => Latex.string "\\bigskip"));
 
 
-(* control style *)
-
-local
-
-fun control_antiquotation name s1 s2 =
+(* nested document text *)
+
+local
+
+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);
         Latex.enclose_block s1 s2 (Thy_Output.output_document ctxt {markdown = false} txt)));
 
 in
 
 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;
 
 
 (* quasi-formal text (unchecked) *)

     theory_text_antiquotation);
 
 end;
 
 
-
-
 (* goal state *)
 
 local
 
 fun goal_state name main =