# HG changeset patch
# User wenzelm
# Date 1726083693 -7200
# Node ID ab0234b9af65925f866fd1cc712dd12b6302abac
# Parent  9de19e3a723155b313ed5d9bdecab8894f0f4037
clarified modules;

diff -r 9de19e3a7231 -r ab0234b9af65 src/Pure/General/latex.ML
--- 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;
diff -r 9de19e3a7231 -r ab0234b9af65 src/Pure/General/print_mode.ML
--- 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;
diff -r 9de19e3a7231 -r ab0234b9af65 src/Pure/Thy/document_antiquotation.ML
--- 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