--- 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 *)
--- 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 */
--- 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;
--- 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))
--- 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>\<open>rail\<close> (Scan.lift Args.text_input)