added emacs mode;
authorwenzelm
Fri Aug 28 14:59:34 1998 +0200 (1998-08-28)
changeset 540683e1e2dadcca
parent 5405 2ecb74e65439
child 5407 b450fea6d70c
added emacs mode;
tuned;
src/Pure/Syntax/token_trans.ML
     1.1 --- a/src/Pure/Syntax/token_trans.ML	Fri Aug 28 14:20:14 1998 +0200
     1.2 +++ b/src/Pure/Syntax/token_trans.ML	Fri Aug 28 14:59:34 1998 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Token translations for xterm and LaTeX output.
     1.8 +Token translations for xterm, emacs and latex output.
     1.9  *)
    1.10  
    1.11  signature TOKEN_TRANS =
    1.12 @@ -37,11 +37,12 @@
    1.13  structure TokenTrans: TOKEN_TRANS =
    1.14  struct
    1.15  
    1.16 +
    1.17  (** misc utils **)
    1.18  
    1.19  fun trans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
    1.20  
    1.21 -val tok_classes = ["class", "tfree", "tvar", "free", "bound", "var"];
    1.22 +val std_token_classes = ["class", "tfree", "tvar", "free", "bound", "var"];
    1.23  
    1.24  
    1.25  
    1.26 @@ -99,18 +100,51 @@
    1.27     ("var", style xterm_color_var)];
    1.28  
    1.29  
    1.30 +
    1.31 +(** emacs output (Isamode) **)
    1.32 +
    1.33 +(* tags *)
    1.34 +
    1.35 +val end_tag = "\^A0";
    1.36 +val tclass_tag = "\^A1";
    1.37 +val tfree_tag = "\^A2";
    1.38 +val tvar_tag = "\^A3";
    1.39 +val free_tag = "\^A4";
    1.40 +val bound_tag = "\^A5";
    1.41 +val var_tag = "\^A6";
    1.42 +
    1.43 +fun tagit p x = (p ^ x ^ end_tag, size x);
    1.44 +
    1.45 +
    1.46 +(* print mode "emacs" *)
    1.47 +
    1.48 +val emacs_trans =
    1.49 + trans_mode "emacs"
    1.50 +  [("class", tagit tclass_tag),
    1.51 +   ("tfree", tagit tfree_tag),
    1.52 +   ("tvar", tagit tvar_tag),
    1.53 +   ("free", tagit free_tag),
    1.54 +   ("bound", tagit bound_tag),
    1.55 +   ("var", tagit var_tag)];
    1.56 +
    1.57 +
    1.58 +
    1.59  (** LaTeX output **)
    1.60  
    1.61  (* FIXME 'a -> \alpha etc. *)
    1.62  
    1.63 +val latex_trans =
    1.64 + trans_mode "latex" [];
    1.65  
    1.66 -(** token translations **)
    1.67 +
    1.68 +
    1.69 +(** standard token translations **)
    1.70  
    1.71  val token_translation =
    1.72 -  map (fn s => ("", s, fn x => (x, size x))) tok_classes @
    1.73 -  (* FIXME tmp test *)
    1.74 -  map (fn s => ("test", s, fn x => (s ^ "[" ^ x ^ "]", size x + size s + 2))) tok_classes @
    1.75 -  xterm_trans;
    1.76 +  map (fn s => ("", s, fn x => (x, size x))) std_token_classes @
    1.77 +  xterm_trans @
    1.78 +  emacs_trans @
    1.79 +  latex_trans;
    1.80  
    1.81  
    1.82  end;