# HG changeset patch
# User wenzelm
# Date 857243390 -3600
# Node ID 3a1fe1c21b777a313e20ea82663c39eb2a82f8a2
# Parent  91a640a91c6eb1f9c9822fc9b8b08de415a72217
added color styles;
refs for test;

diff -r 91a640a91c6e -r 3a1fe1c21b77 src/Pure/Syntax/token_trans.ML
--- a/src/Pure/Syntax/token_trans.ML	Fri Feb 28 21:54:37 1997 +0100
+++ b/src/Pure/Syntax/token_trans.ML	Sat Mar 01 20:09:50 1997 +0100
@@ -8,6 +8,24 @@
 signature TOKEN_TRANS =
 sig
   val token_translation: (string * string * (string -> string * int)) list
+  val class_style: string ref
+  val tfree_style: string ref
+  val tvar_style: string ref
+  val free_style: string ref
+  val bound_style: string ref
+  val var_style: string ref
+  val normal: string
+  val bold: string
+  val underline: string
+  val reverse: string
+  val black: string
+  val red: string
+  val green: string
+  val yellow: string
+  val blue: string
+  val purple: string
+  val cyan: string
+  val white: string
 end;
 
 structure TokenTrans: TOKEN_TRANS =
@@ -28,17 +46,37 @@
 val normal = "\^[[0m";
 val bold = "\^[[1m";
 val underline = "\^[[4m";
+val reverse = "\^[[7m";
+
+val black = "\^[[30m";		(**)
+val red = "\^[[31m";		(**)
+val green = "\^[[32m";		(**)
+val yellow = "\^[[33m";
+val blue = "\^[[34m";		(**)
+val purple = "\^[[35m";		(**)
+val cyan = "\^[[36m";
+val white = "\^[[37m";
 
 fun style s x = (s ^ x ^ normal, size x);
+fun ref_style (ref s) x = (s ^ x ^ normal, size x);
+
+val class_style = ref normal;
+val tfree_style = ref bold;
+val tvar_style = ref bold;
+val free_style = ref bold;
+val bound_style = ref underline;
+val var_style = ref bold;
 
 
 val xterm_trans =
  trans_mode "xterm"
-  [("bound", style underline),
-   ("free", style bold),
-   ("var", style bold),
-   ("tfree", style bold),
-   ("tvar", style bold)];
+  [("class", ref_style class_style),
+   ("tfree", ref_style tfree_style),
+   ("tvar", ref_style tvar_style),
+   ("free", ref_style free_style),
+   ("bound", ref_style bound_style),
+   ("var", ref_style var_style)]
+
 
 (* FIXME xterm-color *)