# HG changeset patch
# User wenzelm
# Date 1636972694 -3600
# Node ID a5c23da73fca82b770214fa89b69796fdee2b94f
# Parent  95e5141378617c0a2ab1d71246d6d4d6cb283aef
clarified signature;

diff -r 95e514137861 -r a5c23da73fca src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sun Nov 14 21:52:13 2021 +0100
+++ b/src/Pure/PIDE/resources.ML	Mon Nov 15 11:38:14 2021 +0100
@@ -418,7 +418,7 @@
   Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) =>
    (check ctxt NONE source;
     Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source))
-    |> Latex.enclose_text "\\isatt{" "}"));
+    |> XML.enclose "\\isatt{" "}"));
 
 fun ML_antiq check =
   Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) =>
diff -r 95e514137861 -r a5c23da73fca src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Sun Nov 14 21:52:13 2021 +0100
+++ b/src/Pure/PIDE/xml.ML	Mon Nov 15 11:38:14 2021 +0100
@@ -34,10 +34,11 @@
       Elem of (string * attributes) * tree list
     | Text of string
   type body = tree list
-  val string: string -> body
   val blob: string list -> body
   val is_empty: tree -> bool
   val is_empty_body: body -> bool
+  val string: string -> body
+  val enclose: string -> string -> body -> body
   val xml_elemN: string
   val xml_nameN: string
   val xml_bodyN: string
@@ -78,9 +79,6 @@
 
 open Output_Primitives.XML;
 
-fun string "" = []
-  | string s = [Text s];
-
 val blob = map Text;
 
 fun is_empty (Text "") = true
@@ -88,6 +86,11 @@
 
 val is_empty_body = forall is_empty;
 
+fun string "" = []
+  | string s = [Text s];
+
+fun enclose bg en body = string bg @ body @ string en;
+
 
 (* wrapped elements *)
 
@@ -157,13 +160,13 @@
 
 fun element name atts body =
   let val b = implode body in
-    if b = "" then enclose "<" "/>" (elem name atts)
-    else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
+    if b = "" then Library.enclose "<" "/>" (elem name atts)
+    else Library.enclose "<" ">" (elem name atts) ^ b ^ Library.enclose "</" ">" name
   end;
 
 fun output_markup (markup as (name, atts)) =
   if Markup.is_empty markup then Markup.no_output
-  else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
+  else (Library.enclose "<" ">" (elem name atts), Library.enclose "</" ">" name);
 
 
 (* output content *)
diff -r 95e514137861 -r a5c23da73fca src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sun Nov 14 21:52:13 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Mon Nov 15 11:38:14 2021 +0100
@@ -46,6 +46,9 @@
 
   def string(s: String): Body = if (s.isEmpty) Nil else List(Text(s))
 
+  def enclose(bg: String, en:String, body: Body): Body =
+    string(bg) ::: body ::: string(en)
+
 
   /* name space */
 
diff -r 95e514137861 -r a5c23da73fca src/Pure/System/scala_compiler.ML
--- a/src/Pure/System/scala_compiler.ML	Sun Nov 14 21:52:13 2021 +0100
+++ b/src/Pure/System/scala_compiler.ML	Mon Nov 15 11:38:14 2021 +0100
@@ -59,7 +59,7 @@
 
 fun scala_name name =
   Latex.string (Latex.output_ascii_breakable "." name)
-  |> Latex.enclose_text "\\isatt{" "}";
+  |> XML.enclose "\\isatt{" "}";
 
 in
 
diff -r 95e514137861 -r a5c23da73fca src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Sun Nov 14 21:52:13 2021 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Mon Nov 15 11:38:14 2021 +0100
@@ -135,7 +135,7 @@
   Document_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input)
     (fn ctxt => fn txt =>
       (Context_Position.reports ctxt (Document_Output.document_reports txt);
-        Latex.enclose_text s1 s2 (Document_Output.output_document ctxt {markdown = false} txt)));
+        XML.enclose s1 s2 (Document_Output.output_document ctxt {markdown = false} txt)));
 
 val _ =
   Theory.setup
@@ -423,7 +423,7 @@
         val _ =
           Context_Position.reports ctxt
             [(pos, Markup.language_url delimited), (pos, Markup.url url)];
-      in Latex.enclose_text "\\url{" "}" (Latex.string (escape_url url)) end));
+      in XML.enclose "\\url{" "}" (Latex.string (escape_url url)) end));
 
 
 (* formal entities *)
@@ -434,7 +434,7 @@
   Document_Output.antiquotation_raw name (Scan.lift Args.name_position)
     (fn ctxt => fn (name, pos) =>
       let val _ = check ctxt (name, pos)
-      in Latex.enclose_text bg en (Latex.string (Output.output name)) end);
+      in XML.enclose bg en (Latex.string (Output.output name)) end);
 
 val _ =
   Theory.setup
diff -r 95e514137861 -r a5c23da73fca src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML	Sun Nov 14 21:52:13 2021 +0100
+++ b/src/Pure/Thy/document_output.ML	Mon Nov 15 11:38:14 2021 +0100
@@ -62,11 +62,11 @@
       Input.cartouche_content syms
       |> output_document (ctxt |> Config.put Document_Antiquotation.thy_output_display false)
           {markdown = false}
-      |> Latex.enclose_text "%\n\\isamarkupcmt{" "%\n}"
+      |> XML.enclose "%\n\\isamarkupcmt{" "%\n}"
   | Comment.Cancel =>
       Symbol_Pos.cartouche_content syms
       |> Latex.symbols_output
-      |> Latex.enclose_text "%\n\\isamarkupcancel{" "}"
+      |> XML.enclose "%\n\\isamarkupcancel{" "}"
   | Comment.Latex => Latex.symbols (Symbol_Pos.cartouche_content syms)
   | Comment.Marker => [])
 and output_comment_document ctxt (comment, syms) =
@@ -122,7 +122,7 @@
         Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) @
           Latex.symbols_output body
     | Antiquote.Antiq {body, ...} =>
-        Latex.enclose_text "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (Latex.symbols_output body));
+        XML.enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (Latex.symbols_output body));
 
 fun output_comment_symbols ctxt {antiq} (comment, syms) =
   (case (comment, antiq) of
@@ -135,7 +135,7 @@
 fun output_body ctxt antiq bg en syms =
   Comment.read_body syms
   |> maps (output_comment_symbols ctxt {antiq = antiq})
-  |> Latex.enclose_text bg en;
+  |> XML.enclose bg en;
 
 in
 
@@ -201,7 +201,7 @@
     Ignore => []
   | Token tok => output_token ctxt tok
   | Heading (cmd, source) =>
-      Latex.enclose_text ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
+      XML.enclose ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
         (output_document ctxt {markdown = false} source)
   | Body (cmd, source) =>
       Latex.environment_text ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)
@@ -485,12 +485,12 @@
 fun isabelle ctxt body =
   if Config.get ctxt Document_Antiquotation.thy_output_display
   then Latex.environment_text "isabelle" body
-  else Latex.enclose_text "\\isa{" "}" body;
+  else XML.enclose "\\isa{" "}" body;
 
 fun isabelle_typewriter ctxt body =
   if Config.get ctxt Document_Antiquotation.thy_output_display
   then Latex.environment_text "isabellett" body
-  else Latex.enclose_text "\\isatt{" "}" body;
+  else XML.enclose "\\isatt{" "}" body;
 
 fun typewriter ctxt s =
   isabelle_typewriter ctxt (Latex.string (Latex.output_ascii s));
diff -r 95e514137861 -r a5c23da73fca src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Sun Nov 14 21:52:13 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Mon Nov 15 11:38:14 2021 +0100
@@ -77,8 +77,8 @@
   {
     def latex_output(latex_text: Text): String = apply(latex_text)
 
-    def latex_macro(name: String, arg: Text): Text =
-      XML.string("\\" + name + "{") ::: arg ::: XML.string("}")
+    def latex_macro(name: String, body: Text): Text =
+      XML.enclose("\\" + name + "{", "}", body)
 
     def index_item(item: Index_Item.Value): String =
     {