# HG changeset patch
# User wenzelm
# Date 1496749358 -7200
# Node ID 08ab52fb9db5c428a6274dfa3304fe06f84a37e7
# Parent  a31760eee09de2329747999b394d89c9c531a89d
tuned signature;

diff -r a31760eee09d -r 08ab52fb9db5 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue Jun 06 13:13:25 2017 +0200
+++ b/src/Pure/Thy/latex.ML	Tue Jun 06 13:42:38 2017 +0200
@@ -24,7 +24,7 @@
   val symbol_source: (string -> bool) * (string -> bool) ->
     string -> Symbol.symbol list -> string
   val theory_entry: string -> string
-  val modes: string list
+  val latexN: string
 end;
 
 structure Latex: LATEX =
@@ -206,7 +206,6 @@
 (* print mode *)
 
 val latexN = "latex";
-val modes = [latexN];
 
 fun latex_output str =
   let val syms = Symbol.explode str
diff -r a31760eee09d -r 08ab52fb9db5 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Jun 06 13:13:25 2017 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Jun 06 13:42:38 2017 +0200
@@ -169,7 +169,7 @@
 
     fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
     val _ = cmd preview_ctxt;
-    val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes;
+    val print_modes = space_explode "," (Config.get print_ctxt modes) @ [Latex.latexN];
   in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
 
 in