src/Pure/Thy/latex.ML
changeset 8965 d46b36785c70
parent 8896 c80aba8c1d5e
child 9038 63d20536971f
--- 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;