src/Pure/Syntax/token_trans.ML
author wenzelm
Wed Oct 31 21:59:07 2001 +0100 (2001-10-31)
changeset 12004 1703de633aaf
parent 11795 12a0fb3ac366
child 12785 27debaf2112d
permissions -rw-r--r--
IsarThy.theorem_i: no locale;
     1 (*  Title:      Pure/Syntax/token_trans.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Token translations for xterm output.
     6 *)
     7 
     8 signature TOKEN_TRANS0 =
     9 sig
    10   val standard_token_classes: string list
    11   val tokentrans_mode: string -> (string * (string -> string * real)) list ->
    12     (string * string * (string -> string * real)) list
    13 end;
    14 
    15 signature TOKEN_TRANS =
    16 sig
    17   include TOKEN_TRANS0
    18   val standard_token_markers: string list
    19   val normal: string
    20   val bold: string
    21   val underline: string
    22   val reverse: string
    23   val black: string
    24   val red: string
    25   val green: string
    26   val yellow: string
    27   val blue: string
    28   val purple: string
    29   val cyan: string
    30   val white: string
    31   val xterm_class: string ref
    32   val xterm_tfree: string ref
    33   val xterm_tvar: string ref
    34   val xterm_free: string ref
    35   val xterm_bound: string ref
    36   val xterm_var: string ref
    37   val xterm_color_class: string ref
    38   val xterm_color_tfree: string ref
    39   val xterm_color_tvar: string ref
    40   val xterm_color_free: string ref
    41   val xterm_color_bound: string ref
    42   val xterm_color_var: string ref
    43   val token_translation: (string * string * (string -> string * real)) list
    44 end;
    45 
    46 structure TokenTrans: TOKEN_TRANS =
    47 struct
    48 
    49 
    50 (** misc utils **)
    51 
    52 fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
    53 
    54 val standard_token_classes =
    55   ["class", "tfree", "tvar", "free", "bound", "var", "num", "xnum", "xstr"];
    56 
    57 val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
    58 
    59 
    60 (** xterm output **)
    61 
    62 (* styles *)
    63 
    64 val normal = "\^[[0m";
    65 val bold = "\^[[1m";
    66 val underline = "\^[[4m";
    67 val reverse = "\^[[7m";
    68 
    69 val black = "\^[[30m";
    70 val red = "\^[[31m";
    71 val green = "\^[[32m";
    72 val yellow = "\^[[33m";
    73 val blue = "\^[[34m";
    74 val purple = "\^[[35m";
    75 val cyan = "\^[[36m";
    76 val white = "\^[[37m";
    77 
    78 fun style (ref s) x = (s ^ x ^ normal, real (size x));
    79 
    80 
    81 (* print modes "xterm" and "xterm_color" *)
    82 
    83 val xterm_class = ref normal;
    84 val xterm_tfree = ref bold;
    85 val xterm_tvar = ref bold;
    86 val xterm_free = ref bold;
    87 val xterm_bound = ref underline;
    88 val xterm_var = ref bold;
    89 
    90 val xterm_color_class = ref red;
    91 val xterm_color_tfree = ref purple;
    92 val xterm_color_tvar = ref purple;
    93 val xterm_color_free = ref blue;
    94 val xterm_color_bound = ref green;
    95 val xterm_color_var = ref blue;
    96 
    97 val xterm_trans =
    98  tokentrans_mode "xterm"
    99   [("class", style xterm_class),
   100    ("tfree", style xterm_tfree),
   101    ("tvar", style xterm_tvar),
   102    ("free", style xterm_free),
   103    ("bound", style xterm_bound),
   104    ("var", style xterm_var)] @
   105  tokentrans_mode "xterm_color"
   106   [("class", style xterm_color_class),
   107    ("tfree", style xterm_color_tfree),
   108    ("tvar", style xterm_color_tvar),
   109    ("free", style xterm_color_free),
   110    ("bound", style xterm_color_bound),
   111    ("var", style xterm_color_var)];
   112 
   113 
   114 
   115 (** standard token translations **)
   116 
   117 val token_translation =
   118   map (fn s => ("", s, fn x => (x, real (size x)))) standard_token_classes @
   119   xterm_trans;
   120 
   121 
   122 end;