# HG changeset patch
# User wenzelm
# Date 1516307368 -3600
# Node ID c23d9375e66118ec6417892e7a9d74726192604f
# Parent  aad5c0982c3da3715a6f60359b910c75cd278cc4
more operations;

diff -r aad5c0982c3d -r c23d9375e661 src/Pure/Thy/latex.ML
--- 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 *)