| changeset 80823 | fb0a9fc3901f |
| parent 80822 | 4f54a509bc89 |
| child 80824 | 0d92bd90be6c |
--- 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