avoid duplicate message for @{action} in particular (see also @{action} within Pure);
--- 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