--- 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
--- 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