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