src/Pure/Syntax/token_trans.ML
author wenzelm
Sun Nov 29 13:16:47 1998 +0100 (1998-11-29)
changeset 5989 9670dae0143d
parent 5408 0a0a35dddabd
child 6322 7047300264c9
permissions -rw-r--r--
proof_general_trans (experimental);
wenzelm@2697
     1
(*  Title:      Pure/Syntax/token_trans.ML
wenzelm@2697
     2
    ID:         $Id$
wenzelm@2697
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@2697
     4
wenzelm@5406
     5
Token translations for xterm, emacs and latex output.
wenzelm@2697
     6
*)
wenzelm@2697
     7
wenzelm@2697
     8
signature TOKEN_TRANS =
wenzelm@2697
     9
sig
wenzelm@2707
    10
  val normal: string
wenzelm@2707
    11
  val bold: string
wenzelm@2707
    12
  val underline: string
wenzelm@2707
    13
  val reverse: string
wenzelm@2707
    14
  val black: string
wenzelm@2707
    15
  val red: string
wenzelm@2707
    16
  val green: string
wenzelm@2707
    17
  val yellow: string
wenzelm@2707
    18
  val blue: string
wenzelm@2707
    19
  val purple: string
wenzelm@2707
    20
  val cyan: string
wenzelm@2707
    21
  val white: string
wenzelm@2710
    22
  val xterm_class: string ref
wenzelm@2710
    23
  val xterm_tfree: string ref
wenzelm@2710
    24
  val xterm_tvar: string ref
wenzelm@2710
    25
  val xterm_free: string ref
wenzelm@2710
    26
  val xterm_bound: string ref
wenzelm@2710
    27
  val xterm_var: string ref
wenzelm@2710
    28
  val xterm_color_class: string ref
wenzelm@2710
    29
  val xterm_color_tfree: string ref
wenzelm@2710
    30
  val xterm_color_tvar: string ref
wenzelm@2710
    31
  val xterm_color_free: string ref
wenzelm@2710
    32
  val xterm_color_bound: string ref
wenzelm@2710
    33
  val xterm_color_var: string ref
wenzelm@2710
    34
  val token_translation: (string * string * (string -> string * int)) list
wenzelm@2697
    35
end;
wenzelm@2697
    36
wenzelm@2697
    37
structure TokenTrans: TOKEN_TRANS =
wenzelm@2697
    38
struct
wenzelm@2697
    39
wenzelm@5406
    40
wenzelm@2697
    41
(** misc utils **)
wenzelm@2697
    42
wenzelm@2697
    43
fun trans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
wenzelm@2697
    44
wenzelm@5406
    45
val std_token_classes = ["class", "tfree", "tvar", "free", "bound", "var"];
wenzelm@2697
    46
wenzelm@2697
    47
wenzelm@2697
    48
wenzelm@2697
    49
(** xterm output **)
wenzelm@2697
    50
wenzelm@2697
    51
(* styles *)
wenzelm@2697
    52
wenzelm@2697
    53
val normal = "\^[[0m";
wenzelm@2697
    54
val bold = "\^[[1m";
wenzelm@2697
    55
val underline = "\^[[4m";
wenzelm@2707
    56
val reverse = "\^[[7m";
wenzelm@2707
    57
wenzelm@2710
    58
val black = "\^[[30m";
wenzelm@2710
    59
val red = "\^[[31m";
wenzelm@2710
    60
val green = "\^[[32m";
wenzelm@2707
    61
val yellow = "\^[[33m";
wenzelm@2710
    62
val blue = "\^[[34m";
wenzelm@2710
    63
val purple = "\^[[35m";
wenzelm@2707
    64
val cyan = "\^[[36m";
wenzelm@2707
    65
val white = "\^[[37m";
wenzelm@2697
    66
wenzelm@2710
    67
fun style (ref s) x = (s ^ x ^ normal, size x);
wenzelm@2710
    68
wenzelm@2710
    69
wenzelm@2710
    70
(* print modes "xterm" and "xterm_color" *)
wenzelm@2707
    71
wenzelm@2710
    72
val xterm_class = ref normal;
wenzelm@2710
    73
val xterm_tfree = ref bold;
wenzelm@2710
    74
val xterm_tvar = ref bold;
wenzelm@2710
    75
val xterm_free = ref bold;
wenzelm@2710
    76
val xterm_bound = ref underline;
wenzelm@2710
    77
val xterm_var = ref bold;
wenzelm@2697
    78
wenzelm@2710
    79
val xterm_color_class = ref red;
wenzelm@2710
    80
val xterm_color_tfree = ref purple;
wenzelm@2710
    81
val xterm_color_tvar = ref purple;
wenzelm@2710
    82
val xterm_color_free = ref blue;
wenzelm@2710
    83
val xterm_color_bound = ref green;
wenzelm@2710
    84
val xterm_color_var = ref blue;
wenzelm@2697
    85
wenzelm@2697
    86
val xterm_trans =
wenzelm@2697
    87
 trans_mode "xterm"
wenzelm@2710
    88
  [("class", style xterm_class),
wenzelm@2710
    89
   ("tfree", style xterm_tfree),
wenzelm@2710
    90
   ("tvar", style xterm_tvar),
wenzelm@2710
    91
   ("free", style xterm_free),
wenzelm@2710
    92
   ("bound", style xterm_bound),
wenzelm@2710
    93
   ("var", style xterm_var)] @
wenzelm@2710
    94
 trans_mode "xterm_color"
wenzelm@2710
    95
  [("class", style xterm_color_class),
wenzelm@2710
    96
   ("tfree", style xterm_color_tfree),
wenzelm@2710
    97
   ("tvar", style xterm_color_tvar),
wenzelm@2710
    98
   ("free", style xterm_color_free),
wenzelm@2710
    99
   ("bound", style xterm_color_bound),
wenzelm@2710
   100
   ("var", style xterm_color_var)];
wenzelm@2697
   101
wenzelm@2697
   102
wenzelm@5406
   103
wenzelm@5406
   104
(** emacs output (Isamode) **)
wenzelm@5406
   105
wenzelm@5989
   106
local
wenzelm@5406
   107
wenzelm@5406
   108
val end_tag = "\^A0";
wenzelm@5406
   109
val tclass_tag = "\^A1";
wenzelm@5406
   110
val tfree_tag = "\^A2";
wenzelm@5406
   111
val tvar_tag = "\^A3";
wenzelm@5406
   112
val free_tag = "\^A4";
wenzelm@5406
   113
val bound_tag = "\^A5";
wenzelm@5406
   114
val var_tag = "\^A6";
wenzelm@5406
   115
wenzelm@5406
   116
fun tagit p x = (p ^ x ^ end_tag, size x);
wenzelm@5406
   117
wenzelm@5989
   118
in
wenzelm@5406
   119
wenzelm@5406
   120
val emacs_trans =
wenzelm@5406
   121
 trans_mode "emacs"
wenzelm@5406
   122
  [("class", tagit tclass_tag),
wenzelm@5406
   123
   ("tfree", tagit tfree_tag),
wenzelm@5406
   124
   ("tvar", tagit tvar_tag),
wenzelm@5406
   125
   ("free", tagit free_tag),
wenzelm@5406
   126
   ("bound", tagit bound_tag),
wenzelm@5406
   127
   ("var", tagit var_tag)];
wenzelm@5406
   128
wenzelm@5989
   129
end;
wenzelm@5989
   130
wenzelm@5989
   131
wenzelm@5989
   132
wenzelm@5989
   133
(** ProofGeneral output **)
wenzelm@5989
   134
wenzelm@5989
   135
local
wenzelm@5989
   136
wenzelm@5989
   137
val end_tag = oct_char "350";
wenzelm@5989
   138
val tclass_tag = oct_char "351";
wenzelm@5989
   139
val tfree_tag = oct_char "352";
wenzelm@5989
   140
val tvar_tag = oct_char "353";
wenzelm@5989
   141
val free_tag = oct_char "354";
wenzelm@5989
   142
val bound_tag = oct_char "355";
wenzelm@5989
   143
val var_tag = oct_char "356";
wenzelm@5989
   144
wenzelm@5989
   145
fun tagit p x = (p ^ x ^ end_tag, size x);
wenzelm@5989
   146
wenzelm@5989
   147
in
wenzelm@5989
   148
wenzelm@5989
   149
val proof_general_trans =
wenzelm@5989
   150
 trans_mode "ProofGeneral"
wenzelm@5989
   151
  [("class", tagit tclass_tag),
wenzelm@5989
   152
   ("tfree", tagit tfree_tag),
wenzelm@5989
   153
   ("tvar", tagit tvar_tag),
wenzelm@5989
   154
   ("free", tagit free_tag),
wenzelm@5989
   155
   ("bound", tagit bound_tag),
wenzelm@5989
   156
   ("var", tagit var_tag)];
wenzelm@5989
   157
wenzelm@5989
   158
end;
wenzelm@5989
   159
wenzelm@5406
   160
wenzelm@5406
   161
wenzelm@2697
   162
(** LaTeX output **)
wenzelm@2697
   163
wenzelm@2697
   164
(* FIXME 'a -> \alpha etc. *)
wenzelm@2697
   165
wenzelm@5406
   166
val latex_trans =
wenzelm@5408
   167
 trans_mode "latex" [] : (string * string * (string -> string * int)) list;
wenzelm@2697
   168
wenzelm@5406
   169
wenzelm@5406
   170
wenzelm@5406
   171
(** standard token translations **)
wenzelm@2697
   172
wenzelm@2697
   173
val token_translation =
wenzelm@5406
   174
  map (fn s => ("", s, fn x => (x, size x))) std_token_classes @
wenzelm@5406
   175
  xterm_trans @
wenzelm@5406
   176
  emacs_trans @
wenzelm@5989
   177
  proof_general_trans @
wenzelm@5406
   178
  latex_trans;
wenzelm@2697
   179
wenzelm@2697
   180
wenzelm@2697
   181
end;