more thorough (potentially duplicate) markup, e.g. relevant for embedded Args syntax within antiquotations;
--- a/src/Pure/Isar/token.ML Wed Mar 05 14:19:54 2014 +0100
+++ b/src/Pure/Isar/token.ML Wed Mar 05 15:24:06 2014 +0100
@@ -336,10 +336,8 @@
(case get_value tok of
NONE => []
| SOME v =>
- if is_kind Keyword tok then []
- else
- let val pos = pos_of tok
- in if Position.is_reported pos then map (pair pos) (value_markup v) else [] end);
+ let val pos = pos_of tok
+ in if Position.is_reported pos then map (pair pos) (value_markup v) else [] end);
(* make values *)