src/Pure/Syntax/token_trans.ML
author paulson
Thu Sep 25 12:09:41 1997 +0200 (1997-09-25)
changeset 3706 e57b5902822f
parent 2710 3b26198fdaa5
child 5406 83e1e2dadcca
permissions -rw-r--r--
Generalized and exported biresolution_from_nets_tac to allow the declaration
of Clarify_tac
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@2697
     5
Token translations for xterm 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@2697
    40
(** misc utils **)
wenzelm@2697
    41
wenzelm@2697
    42
fun trans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
wenzelm@2697
    43
wenzelm@2697
    44
val tok_classes = ["class", "tfree", "tvar", "free", "bound", "var"];
wenzelm@2697
    45
wenzelm@2697
    46
wenzelm@2697
    47
wenzelm@2697
    48
(** xterm output **)
wenzelm@2697
    49
wenzelm@2697
    50
(* styles *)
wenzelm@2697
    51
wenzelm@2697
    52
val normal = "\^[[0m";
wenzelm@2697
    53
val bold = "\^[[1m";
wenzelm@2697
    54
val underline = "\^[[4m";
wenzelm@2707
    55
val reverse = "\^[[7m";
wenzelm@2707
    56
wenzelm@2710
    57
val black = "\^[[30m";
wenzelm@2710
    58
val red = "\^[[31m";
wenzelm@2710
    59
val green = "\^[[32m";
wenzelm@2707
    60
val yellow = "\^[[33m";
wenzelm@2710
    61
val blue = "\^[[34m";
wenzelm@2710
    62
val purple = "\^[[35m";
wenzelm@2707
    63
val cyan = "\^[[36m";
wenzelm@2707
    64
val white = "\^[[37m";
wenzelm@2697
    65
wenzelm@2710
    66
fun style (ref s) x = (s ^ x ^ normal, size x);
wenzelm@2710
    67
wenzelm@2710
    68
wenzelm@2710
    69
(* print modes "xterm" and "xterm_color" *)
wenzelm@2707
    70
wenzelm@2710
    71
val xterm_class = ref normal;
wenzelm@2710
    72
val xterm_tfree = ref bold;
wenzelm@2710
    73
val xterm_tvar = ref bold;
wenzelm@2710
    74
val xterm_free = ref bold;
wenzelm@2710
    75
val xterm_bound = ref underline;
wenzelm@2710
    76
val xterm_var = ref bold;
wenzelm@2697
    77
wenzelm@2710
    78
val xterm_color_class = ref red;
wenzelm@2710
    79
val xterm_color_tfree = ref purple;
wenzelm@2710
    80
val xterm_color_tvar = ref purple;
wenzelm@2710
    81
val xterm_color_free = ref blue;
wenzelm@2710
    82
val xterm_color_bound = ref green;
wenzelm@2710
    83
val xterm_color_var = ref blue;
wenzelm@2697
    84
wenzelm@2697
    85
val xterm_trans =
wenzelm@2697
    86
 trans_mode "xterm"
wenzelm@2710
    87
  [("class", style xterm_class),
wenzelm@2710
    88
   ("tfree", style xterm_tfree),
wenzelm@2710
    89
   ("tvar", style xterm_tvar),
wenzelm@2710
    90
   ("free", style xterm_free),
wenzelm@2710
    91
   ("bound", style xterm_bound),
wenzelm@2710
    92
   ("var", style xterm_var)] @
wenzelm@2710
    93
 trans_mode "xterm_color"
wenzelm@2710
    94
  [("class", style xterm_color_class),
wenzelm@2710
    95
   ("tfree", style xterm_color_tfree),
wenzelm@2710
    96
   ("tvar", style xterm_color_tvar),
wenzelm@2710
    97
   ("free", style xterm_color_free),
wenzelm@2710
    98
   ("bound", style xterm_color_bound),
wenzelm@2710
    99
   ("var", style xterm_color_var)];
wenzelm@2697
   100
wenzelm@2697
   101
wenzelm@2697
   102
(** LaTeX output **)
wenzelm@2697
   103
wenzelm@2697
   104
(* FIXME 'a -> \alpha etc. *)
wenzelm@2697
   105
wenzelm@2697
   106
wenzelm@2697
   107
(** token translations **)
wenzelm@2697
   108
wenzelm@2697
   109
val token_translation =
wenzelm@2697
   110
  map (fn s => ("", s, fn x => (x, size x))) tok_classes @
wenzelm@2697
   111
  (* FIXME tmp test *)
wenzelm@2697
   112
  map (fn s => ("test", s, fn x => (s ^ "[" ^ x ^ "]", size x + size s + 2))) tok_classes @
wenzelm@2697
   113
  xterm_trans;
wenzelm@2697
   114
wenzelm@2697
   115
wenzelm@2697
   116
end;