clarified signature: more explicit type "ops";

--- a/src/Pure/General/latex.ML	Fri Sep 06 20:31:20 2024 +0200
+++ b/src/Pure/General/latex.ML	Mon Sep 09 11:12:13 2024 +0200
@@ -253,11 +253,11 @@
 
 fun latex_escape ss = Symbol.latex :: Symbol.open_ :: ss @ [Symbol.close];
 
-val _ = Output.add_mode latexN latex_output latex_escape;
-val _ = Markup.add_mode latexN latex_markup;
+val _ = Output.add_mode latexN {output = latex_output, escape = latex_escape};
+val _ = Markup.add_mode latexN {output = latex_markup};
 
 val _ = Pretty.add_mode latexN
-  (fn s => fn _ => if s = "" then s else uncurry enclose indent_markup s);
+  {indent = fn s => fn _ => if s = "" then s else uncurry enclose indent_markup s};
 
 end;
 

--- a/src/Pure/General/output.ML	Fri Sep 06 20:31:20 2024 +0200
+++ b/src/Pure/General/output.ML	Mon Sep 09 11:12:13 2024 +0200
@@ -16,9 +16,9 @@
 sig
   include BASIC_OUTPUT
   type output = string
-  val default_output: string -> output * int
-  val default_escape: output list -> string list
-  val add_mode: string -> (string -> output * int) -> (output list -> string list) -> unit
+  type ops = {output: string -> output * int, escape: output list -> string list}
+  val default_ops: ops
+  val add_mode: string -> ops -> unit
   val output_width: string -> output * int
   val output: string -> output
   val escape: output list -> string list
@@ -65,18 +65,18 @@
 
 type output = string;  (*raw system output*)
 
-fun default_output s = (s, size s);
-fun default_escape (ss: output list) = ss;
+type ops = {output: string -> output * int, escape: output list -> string list};
+
+val default_ops: ops = {output = fn s => (s, size s), escape = I};
 
 local
-  val default = {output = default_output, escape = default_escape};
-  val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
+  val modes = Synchronized.var "Output.modes" (Symtab.make [("", default_ops)]);
 in
-  fun add_mode name output escape =
+  fun add_mode name ops =
     if Thread_Data.is_virtual then ()
-    else Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
+    else Synchronized.change modes (Symtab.update_new (name, ops));
   fun get_mode () =
-    the_default default
+    the_default default_ops
       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
 end;
 

--- a/src/Pure/General/pretty.ML	Fri Sep 06 20:31:20 2024 +0200
+++ b/src/Pure/General/pretty.ML	Mon Sep 09 11:12:13 2024 +0200
@@ -20,8 +20,9 @@
 
 signature PRETTY =
 sig
-  val default_indent: string -> int -> Output.output
-  val add_mode: string -> (string -> int -> Output.output) -> unit
+  type ops = {indent: string -> int -> Output.output}
+  val default_ops: ops
+  val add_mode: string -> ops -> unit
   type T
   val to_ML: T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
@@ -88,19 +89,20 @@
 
 (** print mode operations **)
 
-fun default_indent (_: string) = Symbol.spaces;
+type ops = {indent: string -> int -> string};
+
+val default_ops: ops = {indent = K Symbol.spaces};
 
 local
-  val default = {indent = default_indent};
-  val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]);
+  val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default_ops)]);
 in
-  fun add_mode name indent =
+  fun add_mode name ops =
     Synchronized.change modes (fn tab =>
       (if not (Symtab.defined tab name) then ()
        else warning ("Redefining pretty mode " ^ quote name);
-       Symtab.update (name, {indent = indent}) tab));
+       Symtab.update (name, ops) tab));
   fun get_mode () =
-    the_default default
+    the_default default_ops
       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
 end;
 

--- a/src/Pure/PIDE/markup.ML	Fri Sep 06 20:31:20 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon Sep 09 11:12:13 2024 +0200
@@ -277,8 +277,9 @@
   val simp_trace_ignoreN: string
   val simp_trace_cancel: serial -> Properties.T
   type output = Output.output * Output.output
+  type ops = {output: T -> output}
   val no_output: output
-  val add_mode: string -> (T -> output) -> unit
+  val add_mode: string -> ops -> unit
   val output: T -> output
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
@@ -843,19 +844,22 @@
 
 type output = Output.output * Output.output;
 
+type ops = {output: T -> output};
+
+val default_ops: ops = {output = Output_Primitives.markup_fn};
+
 val no_output = ("", "");
 
 local
-  val default = {output = Output_Primitives.markup_fn};
-  val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
+  val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default_ops)]);
 in
-  fun add_mode name output =
+  fun add_mode name ops =
     Synchronized.change modes (fn tab =>
       (if not (Symtab.defined tab name) then ()
        else Output.warning ("Redefining markup mode " ^ quote name);
-       Symtab.update (name, {output = output}) tab));
+       Symtab.update (name, ops) tab));
   fun get_mode () =
-    the_default default
+    the_default default_ops
       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
 end;
 

--- a/src/Pure/PIDE/yxml.ML	Fri Sep 06 20:31:20 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML	Mon Sep 09 11:12:13 2024 +0200
@@ -29,6 +29,7 @@
   val write_body: Path.T -> XML.body -> unit
   val output_markup: Markup.T -> string * string
   val output_markup_elem: Markup.T -> (string * string) * string
+  val markup_ops: Markup.ops
   val parse_body: string -> XML.body
   val parse_body_bytes: Bytes.T -> XML.body
   val parse: string -> XML.tree
@@ -98,6 +99,7 @@
   let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
   in ((bg1, bg2), en) end;
 
+val markup_ops: Markup.ops = {output = output_markup};
 
 
 (** efficient YXML parsing **)

--- a/src/Pure/System/isabelle_process.ML	Fri Sep 06 20:31:20 2024 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Sep 09 11:12:13 2024 +0200
@@ -24,8 +24,8 @@
 
 fun is_active () = Print_Mode.print_mode_active isabelle_processN;
 
-val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
-val _ = Markup.add_mode isabelle_processN YXML.output_markup;
+val _ = Output.add_mode isabelle_processN Output.default_ops;
+val _ = Markup.add_mode isabelle_processN YXML.markup_ops;
 
 val protocol_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
 val protocol_modes2 = [isabelle_processN, Pretty.symbolicN];

--- a/src/Tools/Code/code_printer.ML	Fri Sep 06 20:31:20 2024 +0200
+++ b/src/Tools/Code/code_printer.ML	Mon Sep 09 11:12:13 2024 +0200
@@ -115,7 +115,7 @@
 
 val code_presentationN = "code_presentation";
 val stmt_nameN = "stmt_name";
-val _ = Markup.add_mode code_presentationN YXML.output_markup;
+val _ = Markup.add_mode code_presentationN YXML.markup_ops;
 
 
 (** assembling and printing text pieces **)