--- a/NEWS Tue Sep 10 16:06:38 2024 +0200
+++ b/NEWS Tue Sep 10 19:57:45 2024 +0200
@@ -91,6 +91,26 @@
variants), while the underlying Pretty.output operation supports an
explicit Pretty.output_ops argument for alternative applications.
+* The print_mode "latex" only affects inner syntax variants, while its
+impact on Output/Markup/Pretty operations has been removed. Instead,
+there are explicit operations Latex.output_, Latex.escape, and
+Latex.output_ops. Output.output has been renamed to Output.output_ to
+indicate statically where Isabelle/ML implementations may have to be
+changed. Rare INCOMPATIBILITY for ambitious document antiquotations that
+generate LaTeX source on their own account, instead of using regular
+Pretty.T interfaces. The following operations need to be adjusted as
+follows:
+
+ Output.output
+ becomes Output.output_ or Latex.output_
+ Output.escape
+ is omitted or becomes Latex.escape
+ Pretty.string_of with implicit "latex" print_mode
+ becomes Pretty.string_of_ops with explicit Latex.output_ops
+
+Note that basic Markup.markup cannot be used for Latex output: proper
+Pretty.T operations are required (e.g. Pretty.mark_str).
+
*** System ***