# HG changeset patch
# User wenzelm
# Date 1418204696 -3600
# Node ID 60c134fdd29033ea979636323cdb0371835898d9
# Parent  e68e44836d0440cae4615018b74e9cb22bc60cb4
tuned;

diff -r e68e44836d04 -r 60c134fdd290 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue Dec 09 22:13:48 2014 +0100
+++ b/src/Pure/Isar/token.ML	Wed Dec 10 10:44:56 2014 +0100
@@ -294,25 +294,16 @@
 local
 
 val token_kind_markup =
- fn Command => (Markup.keyword1, "")
-  | Keyword => (Markup.keyword2, "")
-  | Ident => (Markup.empty, "")
-  | Long_Ident => (Markup.empty, "")
-  | Sym_Ident => (Markup.empty, "")
-  | Var => (Markup.var, "")
+ fn Var => (Markup.var, "")
   | Type_Ident => (Markup.tfree, "")
   | Type_Var => (Markup.tvar, "")
-  | Nat => (Markup.empty, "")
-  | Float => (Markup.empty, "")
-  | Space => (Markup.empty, "")
   | String => (Markup.string, "")
   | Alt_String => (Markup.alt_string, "")
   | Verbatim => (Markup.verbatim, "")
   | Cartouche => (Markup.cartouche, "")
   | Comment => (Markup.comment, "")
   | Error msg => (Markup.bad, msg)
-  | Internal_Value => (Markup.empty, "")
-  | EOF => (Markup.empty, "");
+  | _ => (Markup.empty, "");
 
 fun keyword_report tok markup = ((pos_of tok, markup), "");
 
diff -r e68e44836d04 -r 60c134fdd290 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Tue Dec 09 22:13:48 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Wed Dec 10 10:44:56 2014 +0100
@@ -144,20 +144,16 @@
 local
 
 fun token_kind_markup SML =
- fn Keyword => (Markup.empty, "")
-  | Ident => (Markup.empty, "")
-  | Long_Ident => (Markup.empty, "")
-  | Type_Var => (Markup.ML_tvar, "")
+ fn Type_Var => (Markup.ML_tvar, "")
   | Word => (Markup.ML_numeral, "")
   | Int => (Markup.ML_numeral, "")
   | Real => (Markup.ML_numeral, "")
   | Char => (Markup.ML_char, "")
   | String => (if SML then Markup.SML_string else Markup.ML_string, "")
-  | Space => (Markup.empty, "")
   | Cartouche => (Markup.ML_cartouche, "")
   | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
   | Error msg => (Markup.bad, msg)
-  | EOF => (Markup.empty, "");
+  | _ => (Markup.empty, "");
 
 in