--- a/src/Pure/Thy/latex.ML Wed Jan 17 15:30:53 2018 +0100
+++ b/src/Pure/Thy/latex.ML Thu Jan 18 21:29:28 2018 +0100
@@ -11,6 +11,7 @@
val text: string * Position.T -> text
val block: text list -> text
val enclose_body: string -> string -> text list -> text list
+ val enclose_block: string -> string -> text list -> text
val output_text: text list -> string
val output_positions: Position.T -> text list -> string
val output_name: string -> string
@@ -78,6 +79,8 @@
(if bg = "" then [] else [string bg]) @ body @
(if en = "" then [] else [string en]);
+fun enclose_block bg en = block o enclose_body bg en;
+
(* output name for LaTeX macros *)