--- 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) =>
--- 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 *)
--- 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 */
--- 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
--- 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
--- 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));
--- 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 =
{