# HG changeset patch
# User wenzelm
# Date 1505990836 -7200
# Node ID c4cbe609f6a8d939aa0bce459a0b6a71b32ce8bf
# Parent  0879f2045965275d070b5b7f08fd9b1610b27e56
avoid duplicate message for @{action} in particular (see also @{action} within Pure);

diff -r 0879f2045965 -r c4cbe609f6a8 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Thu Sep 21 10:58:34 2017 +0200
+++ b/src/Doc/antiquote_setup.ML	Thu Sep 21 12:47:16 2017 +0200
@@ -177,7 +177,8 @@
             NONE => ""
           | SOME is_def =>
               "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
-        val _ = check ctxt (name, pos);
+        val _ =
+          if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else ();
       in
         idx ^
         (Output.output name