src/Pure/Syntax/token_trans.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 14880 7586233bd4bd
permissions -rw-r--r--
Merged in license change from Isabelle2004
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@6695
     5
Token translations for xterm output.
wenzelm@2697
     6
*)
wenzelm@2697
     7
wenzelm@6322
     8
signature TOKEN_TRANS0 =
wenzelm@6322
     9
sig
wenzelm@6322
    10
  val standard_token_classes: string list
wenzelm@6695
    11
  val tokentrans_mode: string -> (string * (string -> string * real)) list ->
wenzelm@6695
    12
    (string * string * (string -> string * real)) list
wenzelm@6322
    13
end;
wenzelm@6322
    14
wenzelm@2697
    15
signature TOKEN_TRANS =
wenzelm@2697
    16
sig
wenzelm@6322
    17
  include TOKEN_TRANS0
wenzelm@11795
    18
  val standard_token_markers: string list
wenzelm@2707
    19
  val normal: string
wenzelm@2707
    20
  val bold: string
wenzelm@2707
    21
  val underline: string
wenzelm@2707
    22
  val reverse: string
wenzelm@2707
    23
  val black: string
wenzelm@2707
    24
  val red: string
wenzelm@2707
    25
  val green: string
wenzelm@2707
    26
  val yellow: string
wenzelm@2707
    27
  val blue: string
wenzelm@2707
    28
  val purple: string
wenzelm@2707
    29
  val cyan: string
wenzelm@2707
    30
  val white: string
wenzelm@2710
    31
  val xterm_class: string ref
wenzelm@2710
    32
  val xterm_tfree: string ref
wenzelm@2710
    33
  val xterm_tvar: string ref
wenzelm@2710
    34
  val xterm_free: string ref
wenzelm@2710
    35
  val xterm_bound: string ref
wenzelm@2710
    36
  val xterm_var: string ref
wenzelm@2710
    37
  val xterm_color_class: string ref
wenzelm@2710
    38
  val xterm_color_tfree: string ref
wenzelm@2710
    39
  val xterm_color_tvar: string ref
wenzelm@2710
    40
  val xterm_color_free: string ref
wenzelm@2710
    41
  val xterm_color_bound: string ref
wenzelm@2710
    42
  val xterm_color_var: string ref
wenzelm@6322
    43
  val token_translation: (string * string * (string -> string * real)) list
wenzelm@2697
    44
end;
wenzelm@2697
    45
wenzelm@2697
    46
structure TokenTrans: TOKEN_TRANS =
wenzelm@2697
    47
struct
wenzelm@2697
    48
wenzelm@5406
    49
wenzelm@2697
    50
(** misc utils **)
wenzelm@2697
    51
wenzelm@6695
    52
fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
wenzelm@2697
    53
wenzelm@6322
    54
val standard_token_classes =
wenzelm@11697
    55
  ["class", "tfree", "tvar", "free", "bound", "var", "num", "xnum", "xstr"];
wenzelm@2697
    56
wenzelm@11795
    57
val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
wenzelm@2697
    58
wenzelm@2697
    59
wenzelm@2697
    60
(** xterm output **)
wenzelm@2697
    61
wenzelm@2697
    62
(* styles *)
wenzelm@2697
    63
wenzelm@2697
    64
val normal = "\^[[0m";
wenzelm@2697
    65
val bold = "\^[[1m";
wenzelm@2697
    66
val underline = "\^[[4m";
wenzelm@2707
    67
val reverse = "\^[[7m";
wenzelm@2707
    68
wenzelm@2710
    69
val black = "\^[[30m";
wenzelm@2710
    70
val red = "\^[[31m";
wenzelm@2710
    71
val green = "\^[[32m";
wenzelm@2707
    72
val yellow = "\^[[33m";
wenzelm@2710
    73
val blue = "\^[[34m";
wenzelm@2710
    74
val purple = "\^[[35m";
wenzelm@2707
    75
val cyan = "\^[[36m";
wenzelm@2707
    76
val white = "\^[[37m";
wenzelm@2697
    77
wenzelm@14880
    78
fun style (ref s) x = Output.output_width x |> apfst (enclose s normal);
wenzelm@2710
    79
wenzelm@2710
    80
wenzelm@2710
    81
(* print modes "xterm" and "xterm_color" *)
wenzelm@2707
    82
wenzelm@2710
    83
val xterm_class = ref normal;
wenzelm@2710
    84
val xterm_tfree = ref bold;
wenzelm@2710
    85
val xterm_tvar = ref bold;
wenzelm@2710
    86
val xterm_free = ref bold;
wenzelm@2710
    87
val xterm_bound = ref underline;
wenzelm@2710
    88
val xterm_var = ref bold;
wenzelm@2697
    89
wenzelm@2710
    90
val xterm_color_class = ref red;
wenzelm@2710
    91
val xterm_color_tfree = ref purple;
wenzelm@2710
    92
val xterm_color_tvar = ref purple;
wenzelm@2710
    93
val xterm_color_free = ref blue;
wenzelm@2710
    94
val xterm_color_bound = ref green;
wenzelm@2710
    95
val xterm_color_var = ref blue;
wenzelm@2697
    96
wenzelm@2697
    97
val xterm_trans =
wenzelm@6695
    98
 tokentrans_mode "xterm"
wenzelm@2710
    99
  [("class", style xterm_class),
wenzelm@2710
   100
   ("tfree", style xterm_tfree),
wenzelm@2710
   101
   ("tvar", style xterm_tvar),
wenzelm@2710
   102
   ("free", style xterm_free),
wenzelm@2710
   103
   ("bound", style xterm_bound),
wenzelm@2710
   104
   ("var", style xterm_var)] @
wenzelm@6695
   105
 tokentrans_mode "xterm_color"
wenzelm@2710
   106
  [("class", style xterm_color_class),
wenzelm@2710
   107
   ("tfree", style xterm_color_tfree),
wenzelm@2710
   108
   ("tvar", style xterm_color_tvar),
wenzelm@2710
   109
   ("free", style xterm_color_free),
wenzelm@2710
   110
   ("bound", style xterm_color_bound),
wenzelm@2710
   111
   ("var", style xterm_color_var)];
wenzelm@2697
   112
wenzelm@2697
   113
wenzelm@5406
   114
wenzelm@5406
   115
(** standard token translations **)
wenzelm@2697
   116
wenzelm@2697
   117
val token_translation =
wenzelm@14880
   118
  map (fn s => ("", s, Output.output_width)) standard_token_classes @
wenzelm@6695
   119
  xterm_trans;
wenzelm@2697
   120
wenzelm@2697
   121
wenzelm@2697
   122
end;