--- a/src/Pure/General/latex.ML Mon Sep 09 21:23:28 2024 +0200
+++ b/src/Pure/General/latex.ML Mon Sep 09 21:32:11 2024 +0200
@@ -257,7 +257,11 @@
val _ = Markup.add_mode latexN {output = latex_markup};
val _ = Pretty.add_mode latexN
- {indent = fn s => fn _ => if s = "" then s else uncurry enclose indent_markup s};
+ {markup = fn (bg, en) =>
+ (case try YXML.parse (bg ^ en) of
+ SOME (XML.Elem (m, _)) => latex_markup m
+ | _ => Markup.no_output),
+ indent = fn s => fn _ => if s = "" then s else uncurry enclose indent_markup s};
end;