# HG changeset patch
# User wenzelm
# Date 1638716086 -3600
# Node ID 1e84ae3e886e8197903a0ce8966bac627e032aab
# Parent  944d4d616ca0ed7955b161790a4e38d8e5fef346
tuned signature;

diff -r 944d4d616ca0 -r 1e84ae3e886e src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sun Dec 05 12:50:36 2021 +0100
+++ b/src/Pure/Thy/latex.ML	Sun Dec 05 15:54:46 2021 +0100
@@ -14,7 +14,6 @@
   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
   val output_ascii_breakable: string -> string -> string
@@ -57,8 +56,6 @@
 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;
-
 
 (* output name for LaTeX macros *)
 
@@ -195,12 +192,12 @@
 (* theory presentation *)
 
 fun environment_text name =
-  enclose_text
+  XML.enclose
     ("%\n\\begin{" ^ output_name name ^ "}%\n")
     ("%\n\\end{" ^ output_name name ^ "}");
 
 fun isabelle_body name =
-  enclose_text
+  XML.enclose
    ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n")
    "%\n\\end{isabellebody}%\n";
 
diff -r 944d4d616ca0 -r 1e84ae3e886e src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Sun Dec 05 12:50:36 2021 +0100
+++ b/src/Pure/pure_syn.ML	Sun Dec 05 15:54:46 2021 +0100
@@ -43,7 +43,7 @@
   Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
     (Parse.opt_target -- Parse.document_source >>
       Document_Output.document_output
-        {markdown = true, markup = Latex.enclose_text "%\n" "\n"});
+        {markdown = true, markup = XML.enclose "%\n" "\n"});
 
 val _ =
   Outer_Syntax.command ("theory", \<^here>) "begin theory"