--- 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), "");