--- a/src/Pure/General/latex.ML Wed Sep 11 21:25:15 2024 +0200
+++ b/src/Pure/General/latex.ML Wed Sep 11 21:41:33 2024 +0200
@@ -28,7 +28,6 @@
type index_entry = {items: index_item list, def: bool}
val index_entry: index_entry -> text
val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
- val latexN: string
val output_: string -> Output.output
val output_width: string -> Output.output * int
val escape: Output.output -> string
@@ -233,11 +232,6 @@
fold (fn index => setup (index_binding index binding) index) [NONE, SOME true, SOME false];
-(* print mode *)
-
-val latexN = "latex";
-
-
(* markup and formatting *)
val output_ = output_symbols o Symbol.explode;
--- a/src/Pure/General/print_mode.ML Wed Sep 11 21:25:15 2024 +0200
+++ b/src/Pure/General/print_mode.ML Wed Sep 11 21:41:33 2024 +0200
@@ -21,6 +21,7 @@
val internal: string
val ASCII: string
val PIDE: string
+ val latex: string
val setmp: string list -> ('a -> 'b) -> 'a -> 'b
val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
val closure: ('a -> 'b) -> 'a -> 'b
@@ -34,6 +35,7 @@
val internal = "internal";
val ASCII = "ASCII";
val PIDE = "PIDE";
+val latex = "latex";
val print_mode = Unsynchronized.ref ([]: string list);
val print_mode_var = Thread_Data.var () : string list Thread_Data.var;
--- a/src/Pure/Thy/document_antiquotation.ML Wed Sep 11 21:25:15 2024 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML Wed Sep 11 21:41:33 2024 +0200
@@ -182,7 +182,8 @@
val _ = command pos (opts, src) preview_ctxt;
val print_ctxt = Context_Position.set_visible false preview_ctxt;
- val print_modes = space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN];
+ val print_modes =
+ space_explode "," (Config.get print_ctxt thy_output_modes) @ [Print_Mode.latex];
in Print_Mode.with_modes print_modes (fn () => command pos (opts, src) print_ctxt) () end;
in