# HG changeset patch # User wenzelm # Date 1621974519 -7200 # Node ID 466fae6bf22ed6fedda007c2b2c489d6489a1ce0 # Parent 546e1e5916351a045e58936965b89bd0a869680b compose Latex text as XML, output exported YXML in Isabelle/Scala; diff -r 546e1e591635 -r 466fae6bf22e src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Tue May 25 21:44:01 2021 +0200 +++ b/src/Doc/antiquote_setup.ML Tue May 25 22:28:39 2021 +0200 @@ -45,7 +45,7 @@ (Document_Antiquotation.delimit ctxt (Document_Output.pretty_thm ctxt thm))) ^ enclose "\\rulename{" "}" (Output.output name)) #> space_implode "\\par\\smallskip%\n" - #> Latex.string #> single + #> Latex.string #> Document_Output.isabelle ctxt)); diff -r 546e1e591635 -r 466fae6bf22e src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Tue May 25 21:44:01 2021 +0200 +++ b/src/Pure/PIDE/markup.ML Tue May 25 22:28:39 2021 +0200 @@ -138,6 +138,7 @@ val text_foldN: string val text_fold: T val document_markerN: string val document_marker: T val document_tagN: string val document_tag: string -> T + val document_latexN: string val document_latex: T val markdown_paragraphN: string val markdown_paragraph: T val markdown_itemN: string val markdown_item: T val markdown_bulletN: string val markdown_bullet: int -> T @@ -530,6 +531,8 @@ val (document_markerN, document_marker) = markup_elem "document_marker"; val (document_tagN, document_tag) = markup_string "document_tag" nameN; +val (document_latexN, document_latex) = markup_elem "document_latex"; + (* Markdown document structure *) diff -r 546e1e591635 -r 466fae6bf22e src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue May 25 21:44:01 2021 +0200 +++ b/src/Pure/PIDE/markup.scala Tue May 25 22:28:39 2021 +0200 @@ -356,6 +356,8 @@ } } + val DOCUMENT_LATEX = "document_latex" + /* Markdown document structure */ diff -r 546e1e591635 -r 466fae6bf22e src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Tue May 25 21:44:01 2021 +0200 +++ b/src/Pure/PIDE/resources.ML Tue May 25 22:28:39 2021 +0200 @@ -412,10 +412,9 @@ fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => - let - val _ = check ctxt NONE source; - val latex = Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source)); - in Latex.enclose_block "\\isatt{" "}" [latex] end); + (check ctxt NONE source; + Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source)) + |> Latex.enclose_text "\\isatt{" "}")); fun ML_antiq check = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => diff -r 546e1e591635 -r 466fae6bf22e src/Pure/System/scala_compiler.ML --- a/src/Pure/System/scala_compiler.ML Tue May 25 21:44:01 2021 +0200 +++ b/src/Pure/System/scala_compiler.ML Tue May 25 22:28:39 2021 +0200 @@ -58,8 +58,8 @@ val args = Scan.optional (Parse.$$$ "(" |-- arguments --| Parse.$$$ ")") " _"; fun scala_name name = - let val latex = Latex.string (Latex.output_ascii_breakable "." name) - in Latex.enclose_block "\\isatt{" "}" [latex] end; + Latex.string (Latex.output_ascii_breakable "." name) + |> Latex.enclose_text "\\isatt{" "}"; in diff -r 546e1e591635 -r 466fae6bf22e src/Pure/Thy/document_antiquotation.ML --- a/src/Pure/Thy/document_antiquotation.ML Tue May 25 21:44:01 2021 +0200 +++ b/src/Pure/Thy/document_antiquotation.ML Tue May 25 22:28:39 2021 +0200 @@ -33,8 +33,8 @@ val setup_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory val boolean: string -> bool val integer: string -> int - val evaluate: (Symbol_Pos.T list -> Latex.text list) -> Proof.context -> - Antiquote.text_antiquote -> Latex.text list + val evaluate: (Symbol_Pos.T list -> Latex.text) -> Proof.context -> + Antiquote.text_antiquote -> Latex.text val approx_content: Proof.context -> string -> string end; @@ -184,7 +184,7 @@ val print_ctxt = Context_Position.set_visible false preview_ctxt; val print_modes = space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN, Pretty.regularN]; - in [Print_Mode.with_modes print_modes (fn () => command pos (opts, src) print_ctxt) ()] end; + in Print_Mode.with_modes print_modes (fn () => command pos (opts, src) print_ctxt) () end; in diff -r 546e1e591635 -r 466fae6bf22e src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Tue May 25 21:44:01 2021 +0200 +++ b/src/Pure/Thy/document_antiquotations.ML Tue May 25 22:28:39 2021 +0200 @@ -131,7 +131,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_block s1 s2 (Document_Output.output_document ctxt {markdown = false} txt))); + Latex.enclose_text s1 s2 (Document_Output.output_document ctxt {markdown = false} txt))); val _ = Theory.setup @@ -149,7 +149,7 @@ val index_like = Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "is" |-- Args.name --| Parse.$$$ ")"); val index_args = Parse.enum1 "!" (Args.embedded_input -- Scan.option index_like); -fun output_text ctxt = Latex.block o Document_Output.output_document ctxt {markdown = false}; +fun output_text ctxt = Document_Output.output_document ctxt {markdown = false}; fun index binding def = Document_Output.antiquotation_raw binding (Scan.lift index_args) @@ -370,16 +370,17 @@ val main_text = Document_Output.verbatim ctxt ((if kind = "" orelse not show_kind then "" else kind ^ " ") ^ txt0 ^ txt); - val index_text = - index |> Option.map (fn def => - let - val ctxt' = Config.put Document_Antiquotation.thy_output_display false ctxt; - val kind' = if kind = "" then " (ML)" else " (ML " ^ kind ^ ")"; - val txt' = Latex.block [Document_Output.verbatim ctxt' idx, Latex.string kind']; - val like = Document_Antiquotation.approx_content ctxt' idx; - in Latex.index_entry {items = [{text = txt', like = like}], def = def} end); - in Latex.block (the_list index_text @ [main_text]) end); + (case index of + NONE => [] + | SOME def => + let + val ctxt' = Config.put Document_Antiquotation.thy_output_display false ctxt; + val kind' = if kind = "" then " (ML)" else " (ML " ^ kind ^ ")"; + val txt' = Document_Output.verbatim ctxt' idx @ Latex.string kind'; + val like = Document_Antiquotation.approx_content ctxt' idx; + in Latex.index_entry {items = [{text = txt', like = like}], def = def} end); + in index_text @ main_text end); fun antiquotation_ml0 test kind = antiquotation_ml parse_ml0 test kind false; @@ -422,7 +423,7 @@ val _ = Context_Position.reports ctxt [(pos, Markup.language_url delimited), (pos, Markup.url url)]; - in Latex.enclose_block "\\url{" "}" [Latex.string (escape_url url)] end)); + in Latex.enclose_text "\\url{" "}" (Latex.string (escape_url url)) end)); (* formal entities *) @@ -433,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_block bg en [Latex.string (Output.output name)] end); + in Latex.enclose_text bg en (Latex.string (Output.output name)) end); val _ = Theory.setup diff -r 546e1e591635 -r 466fae6bf22e src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Tue May 25 21:44:01 2021 +0200 +++ b/src/Pure/Thy/document_build.scala Tue May 25 22:28:39 2021 +0200 @@ -218,7 +218,8 @@ for (name <- document_theories) yield { val path = Path.basic(tex_name(name)) - val content = get_export(name.theory, document_tex_name(name)).uncompressed + val xml = YXML.parse_body(get_export(name.theory, document_tex_name(name)).text) + val content = Latex.output(xml, file_pos = name.path.implode_symbolic) Content(path, content) } diff -r 546e1e591635 -r 466fae6bf22e src/Pure/Thy/document_output.ML --- a/src/Pure/Thy/document_output.ML Tue May 25 21:44:01 2021 +0200 +++ b/src/Pure/Thy/document_output.ML Tue May 25 22:28:39 2021 +0200 @@ -7,20 +7,18 @@ signature DOCUMENT_OUTPUT = sig val document_reports: Input.source -> Position.report list - val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list + val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text val check_comments: Proof.context -> Symbol_Pos.T list -> unit - val output_token: Proof.context -> Token.T -> Latex.text list - val output_source: Proof.context -> string -> Latex.text list + val output_token: Proof.context -> Token.T -> Latex.text + val output_source: Proof.context -> string -> Latex.text type segment = {span: Command_Span.span, command: Toplevel.transition, prev_state: Toplevel.state, state: Toplevel.state} - val present_thy: Options.T -> theory -> segment list -> Latex.text list + val present_thy: Options.T -> theory -> segment list -> Latex.text val pretty_term: Proof.context -> term -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T - val lines: Latex.text list -> Latex.text list - val items: Latex.text list -> Latex.text list - val isabelle: Proof.context -> Latex.text list -> Latex.text - val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text + val isabelle: Proof.context -> Latex.text -> Latex.text + val isabelle_typewriter: Proof.context -> Latex.text -> Latex.text val typewriter: Proof.context -> string -> Latex.text val verbatim: Proof.context -> string -> Latex.text val source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text @@ -58,25 +56,23 @@ (pos, Markup.plain_text)] end; -val output_symbols = single o Latex.symbols_output; - fun output_comment ctxt (kind, syms) = (case kind of Comment.Comment => Input.cartouche_content syms |> output_document (ctxt |> Config.put Document_Antiquotation.thy_output_display false) {markdown = false} - |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}" + |> Latex.enclose_text "%\n\\isamarkupcmt{" "%\n}" | Comment.Cancel => Symbol_Pos.cartouche_content syms - |> output_symbols - |> Latex.enclose_body "%\n\\isamarkupcancel{" "}" - | Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)] + |> Latex.symbols_output + |> Latex.enclose_text "%\n\\isamarkupcancel{" "}" + | Comment.Latex => Latex.symbols (Symbol_Pos.cartouche_content syms) | Comment.Marker => []) and output_comment_document ctxt (comment, syms) = (case comment of SOME kind => output_comment ctxt (kind, syms) - | NONE => [Latex.symbols syms]) + | NONE => Latex.symbols syms) and output_document_text ctxt syms = Comment.read_body syms |> maps (output_comment_document ctxt) and output_document ctxt {markdown} source = @@ -88,14 +84,15 @@ maps (Document_Antiquotation.evaluate (output_document_text ctxt) ctxt); fun output_line line = - (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @ + (if Markdown.line_is_item line then Latex.string "\\item " else []) @ output_antiquotes (Markdown.line_content line); fun output_block (Markdown.Par lines) = - Latex.block (separate (Latex.string "\n") (map (Latex.block o output_line) lines)) + separate (XML.Text "\n") (map (Latex.block o output_line) lines) | output_block (Markdown.List {kind, body, ...}) = - Latex.environment_block (Markdown.print_kind kind) (output_blocks body) - and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks); + Latex.environment_text (Markdown.print_kind kind) (output_blocks body) + and output_blocks blocks = + separate (XML.Text "\n\n") (map (Latex.block o output_block) blocks); in if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then [] else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms @@ -120,16 +117,16 @@ local val output_symbols_antiq = - (fn Antiquote.Text syms => output_symbols syms + (fn Antiquote.Text syms => Latex.symbols_output syms | Antiquote.Control {name = (name, _), body, ...} => - Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) :: - output_symbols body + Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) @ + Latex.symbols_output body | Antiquote.Antiq {body, ...} => - Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body)); + Latex.enclose_text "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (Latex.symbols_output body)); fun output_comment_symbols ctxt {antiq} (comment, syms) = (case (comment, antiq) of - (NONE, false) => output_symbols syms + (NONE, false) => Latex.symbols_output syms | (NONE, true) => Antiquote.parse_comments (#1 (Symbol_Pos.range syms)) syms |> maps output_symbols_antiq @@ -138,7 +135,7 @@ fun output_body ctxt antiq bg en syms = Comment.read_body syms |> maps (output_comment_symbols ctxt {antiq = antiq}) - |> Latex.enclose_body bg en; + |> Latex.enclose_text bg en; in @@ -203,12 +200,12 @@ Ignore => [] | Token tok => output_token ctxt tok | Heading (cmd, source) => - Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n" + Latex.enclose_text ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n" (output_document ctxt {markdown = false} source) | Body (cmd, source) => - [Latex.environment_block ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)] + Latex.environment_text ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source) | Raw source => - Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]); + Latex.string "%\n" @ output_document ctxt {markdown = true} source @ Latex.string "\n"); (* command spans *) @@ -242,7 +239,7 @@ fun edge which f (x: string option, y) = if x = y then I - else (case which (x, y) of NONE => I | SOME txt => cons (Latex.string (f txt))); + else (case which (x, y) of NONE => I | SOME txt => fold cons (Latex.string (f txt))); val begin_tag = edge #2 Latex.begin_tag; val end_tag = edge #1 Latex.end_tag; @@ -305,7 +302,7 @@ val ctxt' = Toplevel.presentation_context state'; val present = fold (fn (tok, (flag, 0)) => fold cons (present_token ctxt' tok) - #> cons (Latex.string flag) + #> fold cons (Latex.string flag) | _ => I); val Span ((cmd_name, cmd_pos), srcs, span_newline) = span; @@ -484,26 +481,23 @@ (* default output *) -val lines = separate (Latex.string "\\isanewline%\n"); -val items = separate (Latex.string "\\isasep\\isanewline%\n"); - fun isabelle ctxt body = if Config.get ctxt Document_Antiquotation.thy_output_display - then Latex.environment_block "isabelle" body - else Latex.block (Latex.enclose_body "\\isa{" "}" body); + then Latex.environment_text "isabelle" body + else Latex.enclose_text "\\isa{" "}" body; fun isabelle_typewriter ctxt body = if Config.get ctxt Document_Antiquotation.thy_output_display - then Latex.environment_block "isabellett" body - else Latex.block (Latex.enclose_body "\\isatt{" "}" body); + then Latex.environment_text "isabellett" body + else Latex.enclose_text "\\isatt{" "}" body; fun typewriter ctxt s = - isabelle_typewriter ctxt [Latex.string (Latex.output_ascii s)]; + isabelle_typewriter ctxt (Latex.string (Latex.output_ascii s)); fun verbatim ctxt = if Config.get ctxt Document_Antiquotation.thy_output_display then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt - else split_lines #> map (typewriter ctxt) #> lines #> Latex.block; + else split_lines #> map (typewriter ctxt #> Latex.block) #> separate (XML.Text "\\isanewline%\n"); fun token_source ctxt {embedded} tok = if Token.is_kind Token.Cartouche tok andalso embedded andalso @@ -523,13 +517,14 @@ #> isabelle ctxt; fun pretty ctxt = - Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt; + Document_Antiquotation.output ctxt #> Latex.string #> isabelle ctxt; fun pretty_source ctxt embedded src prt = if is_source ctxt then source ctxt embedded src else pretty ctxt prt; fun pretty_items ctxt = - map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt; + map (Document_Antiquotation.output ctxt #> XML.Text) #> + separate (XML.Text "\\isasep\\isanewline%\n") #> isabelle ctxt; fun pretty_items_source ctxt embedded src prts = if is_source ctxt then source ctxt embedded src else pretty_items ctxt prts; diff -r 546e1e591635 -r 466fae6bf22e src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Tue May 25 21:44:01 2021 +0200 +++ b/src/Pure/Thy/latex.ML Tue May 25 22:28:39 2021 +0200 @@ -6,14 +6,13 @@ signature LATEX = sig - type text - val string: string -> text + type text = XML.body 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 string: string -> text + val block: text -> XML.tree + val enclose_text: string -> string -> text -> text + val latex_text: text -> text + val output_text: text -> string val output_name: string -> string val output_ascii: string -> string val output_ascii_breakable: string -> string -> string @@ -25,9 +24,9 @@ val end_delim: string -> string val begin_tag: string -> string val end_tag: string -> string - val environment_block: string -> text list -> text + val environment_text: string -> text -> text val environment: string -> string -> string - val isabelle_body: string -> text list -> text list + val isabelle_body: string -> text -> text val theory_entry: string -> string val index_escape: string -> string type index_item = {text: text, like: string} @@ -45,53 +44,24 @@ (* text with positions *) -abstype text = Text of string * Position.T | Block of text list -with - -fun string s = Text (s, Position.none); -val text = Text; -val block = Block; - -fun map_text f (Text (s, pos)) = Text (f s, pos) - | map_text f (Block texts) = Block ((map o map_text) f texts); +type text = XML.body; -fun output_text texts = - let - fun output (Text (s, _)) = Buffer.add s - | output (Block body) = fold output body; - in Buffer.empty |> fold output texts |> Buffer.content end; +fun text ("", _) = [] + | text (s, pos) = [XML.Elem (Position.markup pos Markup.document_latex, [XML.Text s])]; -fun output_positions file_pos texts = - let - fun position (a, b) = enclose "%:%" "%:%" (a ^ "=" ^ b); - fun add_position p positions = - let val s = position (apply2 Value.print_int p) - in positions |> s <> hd positions ? cons s end; +fun string s = text (s, Position.none); + +fun block body = XML.Elem (Markup.document_latex, body); - fun output (Text (s, pos)) (positions, line) = - let - val positions' = - (case Position.line_of pos of - NONE => positions - | SOME l => add_position (line, l) positions); - val line' = fold_string (fn c => fn n => if c = "\n" then n + 1 else n) s line; - in (positions', line') end - | output (Block body) res = fold output body res; - in - (case Position.file_of file_pos of - NONE => "" - | SOME file => - ([position (Markup.fileN, file), "\\endinput"], 1) - |> fold output texts |> #1 |> rev |> cat_lines) - end; +fun latex_text text = + text |> maps + (fn XML.Elem ((name, _), body) => + if name = Markup.document_latexN then latex_text body else [] + | t => [t]); -end; +val output_text = XML.content_of o latex_text; -fun enclose_body bg en body = - (if bg = "" then [] else [string bg]) @ body @ - (if en = "" then [] else [string en]); - -fun enclose_block bg en = block o enclose_body bg en; +fun enclose_text bg en body = string bg @ body @ string en; (* output name for LaTeX macros *) @@ -240,11 +210,11 @@ ("%\n\\begin{" ^ output_name name ^ "}%\n", "%\n\\end{" ^ output_name name ^ "}"); -fun environment_block name = environment_delim name |-> enclose_body #> block; +fun environment_text name = environment_delim name |-> enclose_text; fun environment name = environment_delim name |-> enclose; fun isabelle_body name = - enclose_body + enclose_text ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n") "%\n\\end{isabellebody}%\n"; @@ -266,7 +236,7 @@ val like_text = if #like item = "" then "" else index_escape (#like item) ^ "@"; - val item_text = index_escape (output_text [#text item]); + val item_text = index_escape (output_text (#text item)); in like_text ^ item_text end; fun index_entry (entry: index_entry) = diff -r 546e1e591635 -r 466fae6bf22e src/Pure/Thy/latex.scala --- a/src/Pure/Thy/latex.scala Tue May 25 21:44:01 2021 +0200 +++ b/src/Pure/Thy/latex.scala Tue May 25 22:28:39 2021 +0200 @@ -28,6 +28,44 @@ } + /* output text and positions */ + + type Text = XML.Body + + def output(latex_text: Text, file_pos: String = ""): String = + { + def position(a: String, b: String): String = "%:%" + a + "=" + b + "%:%" + + var positions: List[String] = + if (file_pos.isEmpty) Nil + else List(position(Markup.FILE, file_pos), "\\endinput") + + var line = 1 + var result = List.empty[String] + + def output(body: XML.Body): Unit = + { + body.foreach { + case XML.Wrapped_Elem(_, _, _) => + case XML.Elem(markup, body) => + if (markup.name == Markup.DOCUMENT_LATEX) { + for { l <- Position.Line.unapply(markup.properties) if positions.nonEmpty } { + val s = position(Value.Int(line), Value.Int(l)) + if (positions.head != s) positions ::= s + } + output(body) + } + case XML.Text(s) => + line += s.count(_ == '\n') + result ::= s + } + } + output(latex_text) + + result.reverse.mkString + cat_lines(positions.reverse) + } + + /* generated .tex file */ private val File_Pattern = """^%:%file=(.+)%:%$""".r diff -r 546e1e591635 -r 466fae6bf22e src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue May 25 21:44:01 2021 +0200 +++ b/src/Pure/Thy/thy_info.ML Tue May 25 22:28:39 2021 +0200 @@ -78,10 +78,8 @@ let val thy_name = Context.theory_name thy; val document_tex_name = document_tex_name thy; - val latex = Latex.isabelle_body thy_name body; - val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; - in Export.export thy document_tex_name (XML.blob output) end + in Export.export thy document_tex_name latex end end)); diff -r 546e1e591635 -r 466fae6bf22e src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML Tue May 25 21:44:01 2021 +0200 +++ b/src/Pure/Tools/rail.ML Tue May 25 22:28:39 2021 +0200 @@ -341,7 +341,7 @@ let val output_antiq = Antiquote.Antiq #> - Document_Antiquotation.evaluate (single o Latex.symbols) ctxt #> + Document_Antiquotation.evaluate Latex.symbols ctxt #> Latex.output_text; fun output_text b s = Output.output s