# 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>\footnote\ "\\footnote{" "}" #> - control_antiquotation \<^binding>\emph\ "\\emph{" "}" #> - control_antiquotation \<^binding>\bold\ "\\textbf{" "}"); + (nested_antiquotation \<^binding>\footnote\ "\\footnote{" "}" #> + nested_antiquotation \<^binding>\emph\ "\\emph{" "}" #> + nested_antiquotation \<^binding>\bold\ "\\textbf{" "}"); end; @@ -203,8 +203,6 @@ end; - - (* goal state *) local