# HG changeset patch
# User wenzelm
# Date 1726049507 -7200
# Node ID e3a419073736037c67c40a77f3a701f3a86f9a57
# Parent  df85df6315af372b513d5debd339705d495bd69c
drop pointless print_mode operations Output.output / Output.escape;

diff -r df85df6315af -r e3a419073736 NEWS
--- a/NEWS	Tue Sep 10 20:36:01 2024 +0200
+++ b/NEWS	Wed Sep 11 12:11:47 2024 +0200
@@ -92,22 +92,12 @@
 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
-
+impact on Output/Markup/Pretty operations has been removed. Thus the
+print_mode operations Output.output and Output.escape have become
+obsolete: superseded by Latex.output_ and Latex.escape specifically for
+LaTeX. Rare INCOMPATIBILITY for ambitious document antiquotations that
+generate Latex source on their own account, instead of using regular
+Pretty.T interfaces (that are based on Latex.output_ops internally).
 Note that basic Markup.markup cannot be used for Latex output: proper
 Pretty.T operations are required (e.g. Pretty.mark_str).
 
diff -r df85df6315af -r e3a419073736 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Tue Sep 10 20:36:01 2024 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Sep 11 12:11:47 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 () => Syntax.string_of_term ctxt t) ()
     val ordered_instances =
       TPTP_Reconstruct.interpret_bindings prob_name thy ordered_binds []
       |> map (snd #> term_to_string)
diff -r df85df6315af -r e3a419073736 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Tue Sep 10 20:36:01 2024 +0200
+++ b/src/Pure/General/output.ML	Wed Sep 11 12:11:47 2024 +0200
@@ -16,12 +16,6 @@
 sig
   include BASIC_OUTPUT
   type output = string
-  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 physical_stdout: output -> unit
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
@@ -61,31 +55,8 @@
 structure Private_Output: PRIVATE_OUTPUT =
 struct
 
-(** print modes **)
-
 type output = string;  (*raw system output*)
 
-type ops = {output: string -> output * int};
-
-val default_ops: ops = {output = fn s => (s, size s)};
-
-local
-  val modes = Synchronized.var "Output.modes" (Symtab.make [("", default_ops)]);
-in
-  fun add_mode name ops =
-    if Thread_Data.is_virtual then ()
-    else Synchronized.change modes (Symtab.update_new (name, ops));
-  fun get_mode () =
-    the_default default_ops
-      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
-end;
-
-fun output_width x = #output (get_mode ()) x;
-val output_ = #1 o output_width;
-
-
-
-(** output channels **)
 
 (* primitives -- provided via bootstrap environment *)
 
@@ -137,19 +108,19 @@
 
 val _ = if Thread_Data.is_virtual then () else init_channels ();
 
-fun writelns ss = ! writeln_fn (map output_ ss);
+fun writelns ss = ! writeln_fn 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 [s];
+fun information s = ! information_fn [s];
+fun tracing s = ! tracing_fn [s];
+fun warning s = ! warning_fn [s];
+fun legacy_feature s = ! legacy_fn [("Legacy feature! " ^ s)];
+fun error_message' (i, s) = ! error_message_fn (i, [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 [s];
+fun status ss = ! status_fn ss;
+fun report ss = ! report_fn ss;
+fun result props ss = ! result_fn props ss;
 fun protocol_message props body = ! protocol_message_fn props body;
 fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => ();
 
diff -r df85df6315af -r e3a419073736 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Sep 10 20:36:01 2024 +0200
+++ b/src/Pure/General/pretty.ML	Wed Sep 11 12:11:47 2024 +0200
@@ -20,7 +20,7 @@
 
 signature PRETTY =
 sig
-  type ops = {markup: Markup.output -> Markup.output, indent: string -> int -> Output.output}
+  type ops = {markup: Markup.output -> Markup.output, indent: string -> int -> Output.output};
   val markup_ops: ops
   val no_markup_ops: ops
   val add_mode: string -> ops -> unit
@@ -71,6 +71,7 @@
     markup: Markup.output -> Markup.output,
     indent: string -> int -> Output.output,
     margin: int}
+  val output_width: string -> Output.output * int
   val output_ops: int option -> output_ops
   val markup_output_ops: int option -> output_ops
   val symbolic_output: T -> Bytes.T
@@ -233,15 +234,16 @@
   indent: string -> int -> Output.output,
   margin: int};
 
+fun output_width s = (s, size s);
+
 fun output_ops opt_margin : output_ops =
   let
-    val {output} = Output.get_mode ();
     val {markup, indent} = get_mode ();
     val margin = ML_Pretty.get_margin opt_margin;
-  in {output = output, markup = markup, indent = indent, margin = margin} end;
+  in {output = output_width, markup = markup, indent = indent, margin = margin} end;
 
 fun markup_output_ops opt_margin : output_ops =
- {output = #output Output.default_ops,
+ {output = output_width,
   markup = #markup markup_ops,
   indent = #indent markup_ops,
   margin = ML_Pretty.get_margin opt_margin};
diff -r df85df6315af -r e3a419073736 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Tue Sep 10 20:36:01 2024 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed Sep 11 12:11:47 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;
+              |> YXML.parse_body;
           in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
       end;
 
diff -r df85df6315af -r e3a419073736 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Sep 10 20:36:01 2024 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Sep 11 12:11:47 2024 +0200
@@ -24,7 +24,6 @@
 
 fun is_active () = Print_Mode.print_mode_active isabelle_processN;
 
-val _ = Output.add_mode isabelle_processN Output.default_ops;
 val _ = Markup.add_mode isabelle_processN YXML.markup_ops;
 val _ = Pretty.add_mode isabelle_processN Pretty.markup_ops;