avoid duplicate message for @{action} in particular (see also @{action} within Pure);
authorwenzelm
Thu Sep 21 12:47:16 2017 +0200 (21 months ago)
changeset 66682c4cbe609f6a8
parent 66681 0879f2045965
child 66683 01189e46dc55
avoid duplicate message for @{action} in particular (see also @{action} within Pure);
src/Doc/antiquote_setup.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Thu Sep 21 10:58:34 2017 +0200
     1.2 +++ b/src/Doc/antiquote_setup.ML	Thu Sep 21 12:47:16 2017 +0200
     1.3 @@ -177,7 +177,8 @@
     1.4              NONE => ""
     1.5            | SOME is_def =>
     1.6                "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
     1.7 -        val _ = check ctxt (name, pos);
     1.8 +        val _ =
     1.9 +          if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else ();
    1.10        in
    1.11          idx ^
    1.12          (Output.output name