# HG changeset patch
# User wenzelm
# Date 1725874891 -7200
# Node ID fb0a9fc3901fc795d4af695106698300b83cebff
# Parent  4f54a509bc8967c888731286823d1d22057c201c
tuned signature;

diff -r 4f54a509bc89 -r fb0a9fc3901f src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Sep 09 11:21:48 2024 +0200
+++ b/src/Pure/General/output.ML	Mon Sep 09 11:41:31 2024 +0200
@@ -19,6 +19,7 @@
   type ops = {output: string -> output * int, escape: output list -> string list}
   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
diff -r 4f54a509bc89 -r fb0a9fc3901f src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Sep 09 11:21:48 2024 +0200
+++ b/src/Pure/General/pretty.ML	Mon Sep 09 11:41:31 2024 +0200
@@ -23,6 +23,7 @@
   type ops = {indent: string -> int -> Output.output}
   val default_ops: ops
   val add_mode: string -> ops -> unit
+  val get_mode: unit -> ops
   type T
   val to_ML: T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
diff -r 4f54a509bc89 -r fb0a9fc3901f src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Sep 09 11:21:48 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon Sep 09 11:41:31 2024 +0200
@@ -280,6 +280,7 @@
   type ops = {output: T -> output}
   val no_output: output
   val add_mode: string -> ops -> unit
+  val get_mode: unit -> ops
   val output: T -> output
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string