proper token_translation for latex mode;
authorwenzelm
Wed May 24 19:09:36 2000 +0200 (2000-05-24)
changeset 8965d46b36785c70
parent 8964 df06ec11bbfa
child 8966 916966f68907
proper token_translation for latex mode;
src/Pure/Thy/latex.ML
src/Pure/pure.ML
     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;
     2.1 --- a/src/Pure/pure.ML	Wed May 24 18:51:28 2000 +0200
     2.2 +++ b/src/Pure/pure.ML	Wed May 24 19:09:36 2000 +0200
     2.3 @@ -15,6 +15,7 @@
     2.4      Calculation.setup @
     2.5      SkipProof.setup @
     2.6      AxClass.setup @
     2.7 +    Latex.setup @
     2.8      Present.setup @
     2.9      Isamode.setup @
    2.10      ProofGeneral.setup;