--- a/src/Doc/antiquote_setup.ML Tue Sep 10 16:06:38 2024 +0200
+++ b/src/Doc/antiquote_setup.ML Tue Sep 10 19:57:45 2024 +0200
@@ -40,10 +40,10 @@
(Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
(fn ctxt =>
map (fn (thm, name) =>
- Output.output
+ Latex.output_
(Document_Antiquotation.format ctxt
(Document_Antiquotation.delimit ctxt (Document_Output.pretty_thm ctxt thm))) ^
- enclose "\\rulename{" "}" (Output.output name))
+ enclose "\\rulename{" "}" (Latex.output_ name))
#> space_implode "\\par\\smallskip%\n"
#> Latex.string
#> Document_Output.isabelle ctxt));
@@ -87,7 +87,7 @@
if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else ();
val latex =
idx ^
- (Output.output name
+ (Latex.output_ name
|> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
|> hyper o enclose "\\mbox{\\isa{" "}}");
in Latex.string latex end);