# HG changeset patch
# User wenzelm
# Date 1394029446 -3600
# Node ID 0ac57f18a4b93a45ab33dc6b7d2f0e324fda0ad4
# Parent  607948c90bf0d92f7696a39e8695cc618b8f70e4
more thorough (potentially duplicate) markup, e.g. relevant for embedded Args syntax within antiquotations;

diff -r 607948c90bf0 -r 0ac57f18a4b9 src/Pure/Isar/token.ML
--- 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 *)