src/Pure/Thy/latex.ML
changeset 8965 d46b36785c70
parent 8896 c80aba8c1d5e
child 9038 63d20536971f
     1.1 --- a/src/Pure/Thy/latex.ML	Wed May 24 18:51:28 2000 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Wed May 24 19:09:36 2000 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4    val old_symbol_source: string -> Symbol.symbol list -> string
     1.5    val token_source: token list -> string
     1.6    val theory_entry: string -> string
     1.7 +  val setup: (theory -> theory) list
     1.8  end;
     1.9  
    1.10  structure Latex: LATEX =
    1.11 @@ -108,11 +109,16 @@
    1.12  
    1.13  (* print mode *)
    1.14  
    1.15 +val latexN = "latex";
    1.16 +
    1.17  fun latex_output str =
    1.18    let val syms = Symbol.explode str
    1.19    in (output_symbols syms, real (Symbol.length syms)) end;
    1.20  
    1.21 -val _ = Symbol.add_mode "latex" latex_output;
    1.22 +val token_translation = map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
    1.23 +
    1.24 +val _ = Symbol.add_mode latexN latex_output;
    1.25 +val setup = [Theory.add_tokentrfuns token_translation];
    1.26  
    1.27  
    1.28  end;