# HG changeset patch
# User wenzelm
# Date 927296665 -7200
# Node ID d3ba5427d56247f99f9e3a79c6d6e3923ad4b79c
# Parent  335833a8b10a50b690f008389d82379eb339a7fc
Isamode and ProofGeneral configuration moved to Pure/Interface;

diff -r 335833a8b10a -r d3ba5427d562 src/Pure/Syntax/token_trans.ML
--- a/src/Pure/Syntax/token_trans.ML	Fri May 21 16:23:48 1999 +0200
+++ b/src/Pure/Syntax/token_trans.ML	Fri May 21 16:24:25 1999 +0200
@@ -2,15 +2,14 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Token translations for xterm, emacs and latex output.
-
-TODO:
-  - elim this file, move stuff to individual print/presentation modes (!?);
+Token translations for xterm output.
 *)
 
 signature TOKEN_TRANS0 =
 sig
   val standard_token_classes: string list
+  val tokentrans_mode: string -> (string * (string -> string * real)) list ->
+    (string * string * (string -> string * real)) list
 end;
 
 signature TOKEN_TRANS =
@@ -49,7 +48,7 @@
 
 (** misc utils **)
 
-fun trans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
+fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
 
 val standard_token_classes =
   ["class", "tfree", "tvar", "free", "bound", "var", "xnum", "xstr"];
@@ -94,14 +93,14 @@
 val xterm_color_var = ref blue;
 
 val xterm_trans =
- trans_mode "xterm"
+ tokentrans_mode "xterm"
   [("class", style xterm_class),
    ("tfree", style xterm_tfree),
    ("tvar", style xterm_tvar),
    ("free", style xterm_free),
    ("bound", style xterm_bound),
    ("var", style xterm_var)] @
- trans_mode "xterm_color"
+ tokentrans_mode "xterm_color"
   [("class", style xterm_color_class),
    ("tfree", style xterm_color_tfree),
    ("tvar", style xterm_color_tvar),
@@ -111,81 +110,11 @@
 
 
 
-(** emacs output (Isamode) **)
-
-local
-
-val end_tag = "\^A0";
-val tclass_tag = "\^A1";
-val tfree_tag = "\^A2";
-val tvar_tag = "\^A3";
-val free_tag = "\^A4";
-val bound_tag = "\^A5";
-val var_tag = "\^A6";
-
-fun tagit p x = (p ^ x ^ end_tag, real (size x));
-
-in
-
-val emacs_trans =
- trans_mode "emacs"
-  [("class", tagit tclass_tag),
-   ("tfree", tagit tfree_tag),
-   ("tvar", tagit tvar_tag),
-   ("free", tagit free_tag),
-   ("bound", tagit bound_tag),
-   ("var", tagit var_tag)];
-
-end;
-
-
-
-(** ProofGeneral output **)
-
-local
-
-val end_tag = oct_char "350";
-val tclass_tag = oct_char "351";
-val tfree_tag = oct_char "352";
-val tvar_tag = oct_char "353";
-val free_tag = oct_char "354";
-val bound_tag = oct_char "355";
-val var_tag = oct_char "356";
-
-fun tagit p x = (p ^ x ^ end_tag, real (size x));
-
-in
-
-val proof_general_trans =
- trans_mode "ProofGeneral"
-  [("class", tagit tclass_tag),
-   ("tfree", tagit tfree_tag),
-   ("tvar", tagit tvar_tag),
-   ("free", tagit free_tag),
-   ("bound", tagit bound_tag),
-   ("var", tagit var_tag)];
-
-end;
-
-
-
-(** LaTeX output **)
-
-(* FIXME 'a -> \alpha etc. *)
-
-val latex_trans =
- trans_mode "latex" [] : (string * string * (string -> string * real)) list;
-
-
-
 (** standard token translations **)
 
 val token_translation =
   map (fn s => ("", s, fn x => (x, real (size x)))) standard_token_classes @
-  xterm_trans @
-  emacs_trans @
-  proof_general_trans @
-  latex_trans;
+  xterm_trans;
 
 
 end;