# HG changeset patch
# User wenzelm
# Date 959188176 -7200
# Node ID d46b36785c70d41a4f23f7df8e58ed8947115132
# Parent  df06ec11bbfa24c8ce14c333661bd742b6e9a073
proper token_translation for latex mode;

diff -r df06ec11bbfa -r d46b36785c70 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed May 24 18:51:28 2000 +0200
+++ b/src/Pure/Thy/latex.ML	Wed May 24 19:09:36 2000 +0200
@@ -13,6 +13,7 @@
   val old_symbol_source: string -> Symbol.symbol list -> string
   val token_source: token list -> string
   val theory_entry: string -> string
+  val setup: (theory -> theory) list
 end;
 
 structure Latex: LATEX =
@@ -108,11 +109,16 @@
 
 (* print mode *)
 
+val latexN = "latex";
+
 fun latex_output str =
   let val syms = Symbol.explode str
   in (output_symbols syms, real (Symbol.length syms)) end;
 
-val _ = Symbol.add_mode "latex" latex_output;
+val token_translation = map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
+
+val _ = Symbol.add_mode latexN latex_output;
+val setup = [Theory.add_tokentrfuns token_translation];
 
 
 end;
diff -r df06ec11bbfa -r d46b36785c70 src/Pure/pure.ML
--- a/src/Pure/pure.ML	Wed May 24 18:51:28 2000 +0200
+++ b/src/Pure/pure.ML	Wed May 24 19:09:36 2000 +0200
@@ -15,6 +15,7 @@
     Calculation.setup @
     SkipProof.setup @
     AxClass.setup @
+    Latex.setup @
     Present.setup @
     Isamode.setup @
     ProofGeneral.setup;