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