tuned -- avoid vacuous reports;
authorwenzelm
Sat Mar 15 11:57:55 2014 +0100 (2014-03-15)
changeset 56160d348378ddf47
parent 56159 39f7b7690de6
child 56161 300f613060b0
tuned -- avoid vacuous reports;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Sat Mar 15 11:28:07 2014 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Sat Mar 15 11:57:55 2014 +0100
     1.3 @@ -464,9 +464,8 @@
     1.4        |> fold (add_name name) accs
     1.5        |> new_entry strict (name, (accs', entry));
     1.6      val _ =
     1.7 -      if proper_pos then
     1.8 -        Context_Position.report_generic context pos
     1.9 -          (entry_markup true (kind_of space) (name, entry))
    1.10 +      if proper_pos andalso Context_Position.is_reported_generic context pos then
    1.11 +        Position.report pos (entry_markup true (kind_of space) (name, entry))
    1.12        else ();
    1.13    in (name, space') end;
    1.14