src/Pure/Syntax/token_trans.ML
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 5408 0a0a35dddabd
child 5989 9670dae0143d
permissions -rw-r--r--
Object logic specific operations.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2697
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Syntax/token_trans.ML
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
     4
5406
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
     5
Token translations for xterm, emacs and latex output.
2697
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
     6
*)
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
     7
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
     8
signature TOKEN_TRANS =
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
     9
sig
2707
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    10
  val normal: string
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    11
  val bold: string
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    12
  val underline: string
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    13
  val reverse: string
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    14
  val black: string
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    15
  val red: string
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    16
  val green: string
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    17
  val yellow: string
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    18
  val blue: string
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    19
  val purple: string
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    20
  val cyan: string
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    21
  val white: string
2710
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    22
  val xterm_class: string ref
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    23
  val xterm_tfree: string ref
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    24
  val xterm_tvar: string ref
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    25
  val xterm_free: string ref
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    26
  val xterm_bound: string ref
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    27
  val xterm_var: string ref
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    28
  val xterm_color_class: string ref
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    29
  val xterm_color_tfree: string ref
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    30
  val xterm_color_tvar: string ref
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    31
  val xterm_color_free: string ref
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    32
  val xterm_color_bound: string ref
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    33
  val xterm_color_var: string ref
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    34
  val token_translation: (string * string * (string -> string * int)) list
2697
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    35
end;
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    36
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    37
structure TokenTrans: TOKEN_TRANS =
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    38
struct
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    39
5406
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
    40
2697
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    41
(** misc utils **)
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    42
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    43
fun trans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    44
5406
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
    45
val std_token_classes = ["class", "tfree", "tvar", "free", "bound", "var"];
2697
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    46
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    47
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    48
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    49
(** xterm output **)
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    50
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    51
(* styles *)
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    52
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    53
val normal = "\^[[0m";
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    54
val bold = "\^[[1m";
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    55
val underline = "\^[[4m";
2707
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    56
val reverse = "\^[[7m";
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    57
2710
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    58
val black = "\^[[30m";
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    59
val red = "\^[[31m";
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    60
val green = "\^[[32m";
2707
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    61
val yellow = "\^[[33m";
2710
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    62
val blue = "\^[[34m";
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    63
val purple = "\^[[35m";
2707
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    64
val cyan = "\^[[36m";
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    65
val white = "\^[[37m";
2697
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    66
2710
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    67
fun style (ref s) x = (s ^ x ^ normal, size x);
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    68
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    69
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    70
(* print modes "xterm" and "xterm_color" *)
2707
3a1fe1c21b77 added color styles;
wenzelm
parents: 2697
diff changeset
    71
2710
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    72
val xterm_class = ref normal;
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    73
val xterm_tfree = ref bold;
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    74
val xterm_tvar = ref bold;
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    75
val xterm_free = ref bold;
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    76
val xterm_bound = ref underline;
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    77
val xterm_var = ref bold;
2697
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    78
2710
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    79
val xterm_color_class = ref red;
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    80
val xterm_color_tfree = ref purple;
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    81
val xterm_color_tvar = ref purple;
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    82
val xterm_color_free = ref blue;
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    83
val xterm_color_bound = ref green;
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    84
val xterm_color_var = ref blue;
2697
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    85
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    86
val xterm_trans =
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
    87
 trans_mode "xterm"
2710
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    88
  [("class", style xterm_class),
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    89
   ("tfree", style xterm_tfree),
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    90
   ("tvar", style xterm_tvar),
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    91
   ("free", style xterm_free),
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    92
   ("bound", style xterm_bound),
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    93
   ("var", style xterm_var)] @
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    94
 trans_mode "xterm_color"
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    95
  [("class", style xterm_color_class),
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    96
   ("tfree", style xterm_color_tfree),
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    97
   ("tvar", style xterm_color_tvar),
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    98
   ("free", style xterm_color_free),
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
    99
   ("bound", style xterm_color_bound),
3b26198fdaa5 improved xterm, xterm_color;
wenzelm
parents: 2707
diff changeset
   100
   ("var", style xterm_color_var)];
2697
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
   101
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
   102
5406
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   103
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   104
(** emacs output (Isamode) **)
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   105
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   106
(* tags *)
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   107
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   108
val end_tag = "\^A0";
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   109
val tclass_tag = "\^A1";
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   110
val tfree_tag = "\^A2";
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   111
val tvar_tag = "\^A3";
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   112
val free_tag = "\^A4";
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   113
val bound_tag = "\^A5";
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   114
val var_tag = "\^A6";
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   115
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   116
fun tagit p x = (p ^ x ^ end_tag, size x);
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   117
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   118
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   119
(* print mode "emacs" *)
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   120
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   121
val emacs_trans =
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   122
 trans_mode "emacs"
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   123
  [("class", tagit tclass_tag),
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   124
   ("tfree", tagit tfree_tag),
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   125
   ("tvar", tagit tvar_tag),
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   126
   ("free", tagit free_tag),
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   127
   ("bound", tagit bound_tag),
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   128
   ("var", tagit var_tag)];
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   129
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   130
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   131
2697
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
   132
(** LaTeX output **)
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
   133
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
   134
(* FIXME 'a -> \alpha etc. *)
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
   135
5406
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   136
val latex_trans =
5408
0a0a35dddabd made SML/NJ happy;
wenzelm
parents: 5406
diff changeset
   137
 trans_mode "latex" [] : (string * string * (string -> string * int)) list;
2697
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
   138
5406
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   139
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   140
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   141
(** standard token translations **)
2697
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
   142
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
   143
val token_translation =
5406
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   144
  map (fn s => ("", s, fn x => (x, size x))) std_token_classes @
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   145
  xterm_trans @
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   146
  emacs_trans @
83e1e2dadcca added emacs mode;
wenzelm
parents: 2710
diff changeset
   147
  latex_trans;
2697
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
   148
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
   149
60999ba189b7 Token translations for xterm and LaTeX output.
wenzelm
parents:
diff changeset
   150
end;