more thorough (potentially duplicate) markup, e.g. relevant for embedded Args syntax within antiquotations;
authorwenzelm
Wed, 05 Mar 2014 15:24:06 +0100
changeset 55916 0ac57f18a4b9
parent 55915 607948c90bf0
child 55917 5438ed05e1c9
more thorough (potentially duplicate) markup, e.g. relevant for embedded Args syntax within antiquotations;
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 *)