tuned signature;
authorwenzelm
Tue Jun 06 13:42:38 2017 +0200 (2017-06-06)
changeset 6602108ab52fb9db5
parent 66020 a31760eee09d
child 66022 cc8e9289a6c4
tuned signature;
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Tue Jun 06 13:13:25 2017 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Tue Jun 06 13:42:38 2017 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    val symbol_source: (string -> bool) * (string -> bool) ->
     1.5      string -> Symbol.symbol list -> string
     1.6    val theory_entry: string -> string
     1.7 -  val modes: string list
     1.8 +  val latexN: string
     1.9  end;
    1.10  
    1.11  structure Latex: LATEX =
    1.12 @@ -206,7 +206,6 @@
    1.13  (* print mode *)
    1.14  
    1.15  val latexN = "latex";
    1.16 -val modes = [latexN];
    1.17  
    1.18  fun latex_output str =
    1.19    let val syms = Symbol.explode str
     2.1 --- a/src/Pure/Thy/thy_output.ML	Tue Jun 06 13:13:25 2017 +0200
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Jun 06 13:42:38 2017 +0200
     2.3 @@ -169,7 +169,7 @@
     2.4  
     2.5      fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
     2.6      val _ = cmd preview_ctxt;
     2.7 -    val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes;
     2.8 +    val print_modes = space_explode "," (Config.get print_ctxt modes) @ [Latex.latexN];
     2.9    in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
    2.10  
    2.11  in