# HG changeset patch # User wenzelm # Date 1636908401 -3600 # Node ID d2522bb4db1bf15c7160a0f6b969d6338c739217 # Parent 47f565849e71d74794bc5382fc97a3addb2f602d symbolic latex_output via XML, interpreted in Isabelle/Scala; diff -r 47f565849e71 -r d2522bb4db1b src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sun Nov 14 15:42:38 2021 +0100 +++ b/src/Pure/PIDE/markup.ML Sun Nov 14 17:46:41 2021 +0100 @@ -149,6 +149,7 @@ 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 latex_outputN: string val latex_output: 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 @@ -569,8 +570,13 @@ val (document_markerN, document_marker) = markup_elem "document_marker"; val (document_tagN, document_tag) = markup_string "document_tag" nameN; + +(* LaTeX *) + val (document_latexN, document_latex) = markup_elem "document_latex"; +val (latex_outputN, latex_output) = markup_elem "latex_output"; + (* Markdown document structure *) diff -r 47f565849e71 -r d2522bb4db1b src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sun Nov 14 15:42:38 2021 +0100 +++ b/src/Pure/PIDE/markup.scala Sun Nov 14 17:46:41 2021 +0100 @@ -366,8 +366,13 @@ val UNIMPORTANT = "unimportant" } + + /* LaTeX */ + val Document_Latex = new Markup_Elem("document_latex") + val Latex_Output = new Markup_Elem("latex_output") + /* Markdown document structure */ diff -r 47f565849e71 -r d2522bb4db1b src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Sun Nov 14 15:42:38 2021 +0100 +++ b/src/Pure/Thy/latex.ML Sun Nov 14 17:46:41 2021 +0100 @@ -10,6 +10,7 @@ val text: string * Position.T -> text val string: string -> text val block: text -> XML.tree + val output: text -> text val enclose_text: string -> string -> text -> text val output_text: text -> string val output_name: string -> string @@ -53,12 +54,15 @@ fun block body = XML.Elem (Markup.document_latex, body); +fun output body = [XML.Elem (Markup.latex_output, body)]; + val output_text = let fun document_latex text = text |> maps (fn XML.Elem ((name, _), body) => - if name = Markup.document_latexN then document_latex body else [] + if name = Markup.document_latexN orelse name = Markup.latex_outputN + then document_latex body else [] | t => [t]) in XML.content_of o document_latex end; diff -r 47f565849e71 -r d2522bb4db1b src/Pure/Thy/latex.scala --- a/src/Pure/Thy/latex.scala Sun Nov 14 15:42:38 2021 +0100 +++ b/src/Pure/Thy/latex.scala Sun Nov 14 17:46:41 2021 +0100 @@ -28,6 +28,8 @@ class Output { + def latex_output(latex_text: Text): Text = List(XML.Text(apply(latex_text))) + def apply(latex_text: Text, file_pos: String = ""): String = { var line = 1 @@ -40,6 +42,8 @@ case XML.Text(s) => line += s.count(_ == '\n') result += s + case XML.Elem(Markup.Latex_Output(_), body) => + traverse(latex_output(body)) case XML.Elem(Markup.Document_Latex(props), body) => for { l <- Position.Line.unapply(props) if positions.nonEmpty } { val s = position(Value.Int(line), Value.Int(l)) diff -r 47f565849e71 -r d2522bb4db1b src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML Sun Nov 14 15:42:38 2021 +0100 +++ b/src/Pure/Tools/rail.ML Sun Nov 14 17:46:41 2021 +0100 @@ -341,47 +341,51 @@ let val output_antiq = Antiquote.Antiq #> - Document_Antiquotation.evaluate Latex.symbols ctxt #> - Latex.output_text; + Document_Antiquotation.evaluate Latex.symbols ctxt; fun output_text b s = Output.output s |> b ? enclose "\\isakeyword{" "}" - |> enclose "\\isa{" "}"; + |> enclose "\\isa{" "}" + |> Latex.string; fun output_cat c (Cat (_, rails)) = outputs c rails and outputs c [rail] = output c rail - | outputs _ rails = implode (map (output "") rails) - and output _ (Bar []) = "" + | outputs _ rails = maps (output "") rails + and output _ (Bar []) = [] | output c (Bar [cat]) = output_cat c cat | output _ (Bar (cat :: cats)) = - "\\rail@bar\n" ^ output_cat "" cat ^ - implode (map (fn Cat (y, rails) => - "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^ - "\\rail@endbar\n" + Latex.string ("\\rail@bar\n") @ output_cat "" cat @ + maps (fn Cat (y, rails) => + Latex.string ("\\rail@nextbar{" ^ string_of_int y ^ "}\n") @ outputs "" rails) cats @ + Latex.string "\\rail@endbar\n" | output c (Plus (cat, Cat (y, rails))) = - "\\rail@plus\n" ^ output_cat c cat ^ - "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^ - "\\rail@endplus\n" - | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n" - | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text false s ^ "}[]\n" - | output c (Terminal (b, s)) = "\\rail@" ^ c ^ "term{" ^ output_text b s ^ "}[]\n" + Latex.string "\\rail@plus\n" @ output_cat c cat @ + Latex.string ("\\rail@nextplus{" ^ string_of_int y ^ "}\n") @ outputs "c" rails @ + Latex.string "\\rail@endplus\n" + | output _ (Newline y) = Latex.string ("\\rail@cr{" ^ string_of_int y ^ "}\n") + | output c (Nonterminal s) = + Latex.string ("\\rail@" ^ c ^ "nont{") @ output_text false s @ Latex.string "}[]\n" + | output c (Terminal (b, s)) = + Latex.string ("\\rail@" ^ c ^ "term{") @ output_text b s @ Latex.string "}[]\n" | output c (Antiquote (b, a)) = - "\\rail@" ^ c ^ (if b then "term{" else "nont{") ^ output_antiq a ^ "}[]\n"; + Latex.string ("\\rail@" ^ c ^ (if b then "term{" else "nont{")) @ + Latex.output (output_antiq a) @ + Latex.string "}[]\n"; fun output_rule (name, rail) = let val (rail', y') = vertical_range rail 0; val out_name = (case name of - Antiquote.Text "" => "" + Antiquote.Text "" => [] | Antiquote.Text s => output_text false s | Antiquote.Antiq a => output_antiq a); in - "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^ - output "" rail' ^ - "\\rail@end\n" + Latex.string ("\\rail@begin{" ^ string_of_int y' ^ "}{") @ out_name @ Latex.string "}\n" @ + output "" rail' @ + Latex.string "\\rail@end\n" end; - in Latex.environment_text "railoutput" (Latex.string (implode (map output_rule rules))) end; + in Latex.environment_text "railoutput" (maps output_rule rules) end; val _ = Theory.setup (Document_Output.antiquotation_raw_embedded \<^binding>\rail\ (Scan.lift Args.text_input)