src/Pure/PIDE/markup.ML
changeset 80823 fb0a9fc3901f
parent 80821 eb383d50564b
child 80826 7feaa04d332b
--- 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