tuned signature;
authorwenzelm
Tue, 06 Jun 2017 13:42:38 +0200
changeset 66021 08ab52fb9db5
parent 66020 a31760eee09d
child 66022 cc8e9289a6c4
tuned signature;
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.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
--- 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