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