--- 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";
--- 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"