clarified print mode "latex": no longer impact Output/Markup/Pretty operations;
renamed Output.output to Output.output_;
removed Output.escape;

--- 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 ***
 

--- 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);

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Tue Sep 10 16:06:38 2024 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Tue Sep 10 19:57:45 2024 +0200
@@ -422,7 +422,7 @@
     val thy = Proof_Context.theory_of ctxt
     fun term_to_string t =
         Print_Mode.with_modes [""]
-          (fn () => Output.output (Syntax.string_of_term ctxt t)) ()
+          (fn () => Output.output_ (Syntax.string_of_term ctxt t)) ()
     val ordered_instances =
       TPTP_Reconstruct.interpret_bindings prob_name thy ordered_binds []
       |> map (snd #> term_to_string)

--- a/src/Pure/General/latex.ML	Tue Sep 10 16:06:38 2024 +0200
+++ b/src/Pure/General/latex.ML	Tue Sep 10 19:57:45 2024 +0200
@@ -29,6 +29,10 @@
   val index_entry: index_entry -> text
   val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
   val latexN: string
+  val output_: string -> Output.output
+  val output_width: string -> Output.output * int
+  val escape: Output.output -> string
+  val output_ops: int option -> Pretty.output_ops
 end;
 
 structure Latex: LATEX =
@@ -233,18 +237,23 @@
 
 val latexN = "latex";
 
+
+(* markup and formatting *)
+
+val output_ = output_symbols o Symbol.explode;
+
+fun output_width str =
+  let val syms = Symbol.explode str
+  in (output_symbols syms, length_symbols syms) end;
+
+val escape = enclose (Symbol.latex ^ Symbol.open_) Symbol.close;
+
 local
 
 val command_markup = YXML.output_markup (Markup.latex_macro "isacommand");
 val keyword_markup = YXML.output_markup (Markup.latex_macro "isakeyword");
 val indent_markup = YXML.output_markup (Markup.latex_macro "isaindent");
 
-fun latex_output str =
-  let val syms = Symbol.explode str
-  in (output_symbols syms, length_symbols syms) end;
-
-fun latex_escape ss = Symbol.latex :: Symbol.open_ :: ss @ [Symbol.close];
-
 fun latex_markup (s, _: Properties.T) =
   if member (op =) [Markup.commandN, Markup.keyword1N, Markup.keyword3N] s then command_markup
   else if s = Markup.keyword2N then keyword_markup
@@ -260,9 +269,11 @@
 
 in
 
-val _ = Output.add_mode latexN {output = latex_output, escape = latex_escape};
-val _ = Markup.add_mode latexN {output = latex_markup};
-val _ = Pretty.add_mode latexN {markup = latex_markup_output, indent = latex_indent};
+fun output_ops opt_margin : Pretty.output_ops =
+ {output = output_width,
+  markup = latex_markup_output,
+  indent = latex_indent,
+  margin = ML_Pretty.get_margin opt_margin};
 
 end;
 

--- a/src/Pure/General/output.ML	Tue Sep 10 16:06:38 2024 +0200
+++ b/src/Pure/General/output.ML	Tue Sep 10 19:57:45 2024 +0200
@@ -16,13 +16,12 @@
 sig
   include BASIC_OUTPUT
   type output = string
-  type ops = {output: string -> output * int, escape: output list -> string list}
+  type ops = {output: string -> output * int}
   val default_ops: ops
   val add_mode: string -> ops -> unit
   val get_mode: unit -> ops
   val output_width: string -> output * int
-  val output: string -> output
-  val escape: output list -> string list
+  val output_: string -> output
   val physical_stdout: output -> unit
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
@@ -66,9 +65,9 @@
 
 type output = string;  (*raw system output*)
 
-type ops = {output: string -> output * int, escape: output list -> string list};
+type ops = {output: string -> output * int};
 
-val default_ops: ops = {output = fn s => (s, size s), escape = I};
+val default_ops: ops = {output = fn s => (s, size s)};
 
 local
   val modes = Synchronized.var "Output.modes" (Symtab.make [("", default_ops)]);
@@ -82,9 +81,7 @@
 end;
 
 fun output_width x = #output (get_mode ()) x;
-val output = #1 o output_width;
-
-fun escape x = #escape (get_mode ()) x;
+val output_ = #1 o output_width;
 
 
 
@@ -140,19 +137,19 @@
 
 val _ = if Thread_Data.is_virtual then () else init_channels ();
 
-fun writelns ss = ! writeln_fn (map output ss);
+fun writelns ss = ! writeln_fn (map output_ ss);
 fun writeln s = writelns [s];
-fun state s = ! state_fn [output s];
-fun information s = ! information_fn [output s];
-fun tracing s = ! tracing_fn [output s];
-fun warning s = ! warning_fn [output s];
-fun legacy_feature s = ! legacy_fn [output ("Legacy feature! " ^ s)];
-fun error_message' (i, s) = ! error_message_fn (i, [output s]);
+fun state s = ! state_fn [output_ s];
+fun information s = ! information_fn [output_ s];
+fun tracing s = ! tracing_fn [output_ s];
+fun warning s = ! warning_fn [output_ s];
+fun legacy_feature s = ! legacy_fn [output_ ("Legacy feature! " ^ s)];
+fun error_message' (i, s) = ! error_message_fn (i, [output_ s]);
 fun error_message s = error_message' (serial (), s);
-fun system_message s = ! system_message_fn [output s];
-fun status ss = ! status_fn (map output ss);
-fun report ss = ! report_fn (map output ss);
-fun result props ss = ! result_fn props (map output ss);
+fun system_message s = ! system_message_fn [output_ s];
+fun status ss = ! status_fn (map output_ ss);
+fun report ss = ! report_fn (map output_ ss);
+fun result props ss = ! result_fn props (map output_ ss);
 fun protocol_message props body = ! protocol_message_fn props body;
 fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => ();
 

--- a/src/Pure/General/pretty.ML	Tue Sep 10 16:06:38 2024 +0200
+++ b/src/Pure/General/pretty.ML	Tue Sep 10 19:57:45 2024 +0200
@@ -68,7 +68,6 @@
   val unbreakable: T -> T
   type output_ops =
    {output: string -> Output.output * int,
-    escape: Output.output list -> string list,
     markup: Markup.output -> Markup.output,
     indent: string -> int -> Output.output,
     margin: int}
@@ -231,21 +230,19 @@
 
 type output_ops =
  {output: string -> Output.output * int,
-  escape: Output.output list -> string list,
   markup: Markup.output -> Markup.output,
   indent: string -> int -> Output.output,
   margin: int};
 
 fun output_ops opt_margin : output_ops =
   let
-    val {output, escape} = Output.get_mode ();
+    val {output} = Output.get_mode ();
     val {markup, indent} = get_mode ();
     val margin = ML_Pretty.get_margin opt_margin;
-  in {output = output, escape = escape, markup = markup, indent = indent, margin = margin} end;
+  in {output = output, markup = markup, indent = indent, margin = margin} end;
 
 fun markup_output_ops opt_margin : output_ops =
  {output = #output Output.default_ops,
-  escape = #escape Output.default_ops,
   markup = #markup markup_ops,
   indent = #indent markup_ops,
   margin = ML_Pretty.get_margin opt_margin};
@@ -454,8 +451,7 @@
   in Buffer.build o out o output_tree ops false end;
 
 fun unformatted_string_of prt =
-  let val ops = output_ops NONE
-  in implode (#escape ops (Buffer.contents (unformatted ops prt))) end;
+  Buffer.content (unformatted (output_ops NONE) prt);
 
 
 (* output interfaces *)
@@ -470,12 +466,12 @@
 
 val output = Buffer.contents oo output_buffer;
 
-fun string_of_ops ops = implode o #escape ops o output ops;
+fun string_of_ops ops = implode o output ops;
 fun string_of prt = string_of_ops (output_ops NONE) prt;
 
 fun writeln prt =
   let val ops = output_ops NONE
-  in Output.writelns (#escape ops (output ops prt)) end;
+  in Output.writelns (output ops prt) end;
 
 
 (* chunks *)

--- a/src/Pure/ML/ml_compiler.ML	Tue Sep 10 16:06:38 2024 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Tue Sep 10 19:57:45 2024 +0200
@@ -67,7 +67,7 @@
             val xml =
               PolyML.NameSpace.Values.printType (types, depth, SOME name_space)
               |> Pretty.from_ML |> Pretty.string_of
-              |> Output.output |> YXML.parse_body;
+              |> Output.output_ |> YXML.parse_body;
           in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
       end;
 

--- a/src/Pure/PIDE/markup.ML	Tue Sep 10 16:06:38 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Sep 10 19:57:45 2024 +0200
@@ -864,9 +864,7 @@
 
 fun output m = if is_empty m then no_output else #output (get_mode ()) m;
 
-fun markup m =
-  let val (bg, en) = output m |> apply2 (single #> Output.escape #> implode);
-  in Library.enclose bg en end;
+fun markup m = output m |-> Library.enclose;
 
 val markups = fold_rev markup;
 

--- a/src/Pure/Thy/document_antiquotation.ML	Tue Sep 10 16:06:38 2024 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML	Tue Sep 10 19:57:45 2024 +0200
@@ -85,10 +85,10 @@
 fun format ctxt =
   let
     val breakable = Config.get ctxt thy_output_display orelse Config.get ctxt thy_output_break;
-    val ops = Pretty.output_ops (SOME (Config.get ctxt thy_output_margin));
-  in not breakable ? Pretty.unbreakable #> Pretty.string_of_ops ops end;
+    val ops = Latex.output_ops (SOME (Config.get ctxt thy_output_margin));
+  in not breakable ? Pretty.unbreakable #> Pretty.output ops #> implode #> Latex.escape end;
 
-fun output ctxt = delimit ctxt #> indent ctxt #> format ctxt #> Output.output;
+fun output ctxt = delimit ctxt #> indent ctxt #> format ctxt #> Latex.output_;
 
 
 (* theory data *)

--- a/src/Pure/Thy/document_antiquotations.ML	Tue Sep 10 16:06:38 2024 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Tue Sep 10 19:57:45 2024 +0200
@@ -434,7 +434,7 @@
   Document_Output.antiquotation_raw name (Scan.lift Args.name_position)
     (fn ctxt => fn (name, pos) =>
       let val _ = check ctxt (name, pos)
-      in Latex.macro macro (Latex.string (Output.output name)) end);
+      in Latex.macro macro (Latex.string (Latex.output_ name)) end);
 
 val _ =
   Theory.setup

--- a/src/Pure/Tools/rail.ML	Tue Sep 10 16:06:38 2024 +0200
+++ b/src/Pure/Tools/rail.ML	Tue Sep 10 19:57:45 2024 +0200
@@ -332,7 +332,7 @@
       Antiquote.Antiq #>
       Document_Antiquotation.evaluate Latex.symbols ctxt;
     fun output_text b s =
-      Latex.string (Output.output s)
+      Latex.string (Latex.output_ s)
       |> b ? Latex.macro "isakeyword"
       |> Latex.macro "isa";