--- a/src/Pure/Thy/latex.ML Mon Nov 15 11:38:14 2021 +0100
+++ b/src/Pure/Thy/latex.ML Mon Nov 15 17:26:31 2021 +0100
@@ -11,6 +11,9 @@
val string: string -> text
val block: text -> XML.tree
val output: text -> text
+ val macro0: string -> text
+ val macro: string -> text -> text
+ val environment: string -> text -> text
val enclose_text: string -> string -> text -> text
val output_name: string -> string
val output_ascii: string -> string
@@ -54,6 +57,10 @@
fun output body = [XML.Elem (Markup.latex_output, body)];
+fun macro0 name = [XML.Elem (Markup.latex_macro0 name, [])];
+fun macro name body = [XML.Elem (Markup.latex_macro name, body)];
+fun environment name body = [XML.Elem (Markup.latex_environment name, body)];
+
fun enclose_text bg en body = string bg @ body @ string en;