no token translation / setup for Latex;
authorwenzelm
Sun, 06 Jun 2004 18:35:11 +0200
changeset 14879 8989eedf72a1
parent 14878 b884a7ba7238
child 14880 7586233bd4bd
no token translation / setup for Latex;
src/Pure/Thy/latex.ML
src/Pure/pure.ML
--- a/src/Pure/Thy/latex.ML	Sun Jun 06 14:20:03 2004 +0200
+++ b/src/Pure/Thy/latex.ML	Sun Jun 06 18:35:11 2004 +0200
@@ -17,7 +17,6 @@
   val old_symbol_source: string -> Symbol.symbol list -> string
   val theory_entry: string -> string
   val modes: string list
-  val setup: (theory -> theory) list
 end;
 
 structure Latex: LATEX =
@@ -149,11 +148,7 @@
 fun latex_indent "" = ""
   | latex_indent s = enclose "\\isaindent{" "}" s;
 
-val token_translation =
-  map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
-
 val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.default_raw);
-val setup = [Theory.add_tokentrfuns token_translation];
 
 
 end;
--- a/src/Pure/pure.ML	Sun Jun 06 14:20:03 2004 +0200
+++ b/src/Pure/pure.ML	Sun Jun 06 18:35:11 2004 +0200
@@ -19,7 +19,6 @@
     Calculation.setup @
     SkipProof.setup @
     AxClass.setup @
-    Latex.setup @
     Present.setup @
     ProofGeneral.setup @
     Codegen.setup @