completion is part of error (not report) and thus not subject to context visibility -- e.g. relevant for 'fixes' in long statements;
authorwenzelm
Thu Mar 06 20:26:43 2014 +0100 (2014-03-06)
changeset 55961c2d4a3608441
parent 55960 beef468837b1
child 55962 fbd0e768bc8f
completion is part of error (not report) and thus not subject to context visibility -- e.g. relevant for 'fixes' in long statements;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Thu Mar 06 19:55:08 2014 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Mar 06 20:26:43 2014 +0100
     1.3 @@ -205,7 +205,7 @@
     1.4  (* completion *)
     1.5  
     1.6  fun completion context space (xname, pos) =
     1.7 -  if Context_Position.is_reported_generic context pos then
     1.8 +  if Position.is_reported pos then
     1.9      let
    1.10        val x = Name.clean xname;
    1.11        val Name_Space {kind = k, internals, ...} = space;