src/Pure/General/name_space.ML

 
 
 (* completion *)
 
 fun completion context space (xname, pos) =
-  if Context_Position.is_visible_generic context andalso Position.is_reported pos
-  then
+  if Context_Position.is_reported_generic context pos then
     let
       val x = Name.clean xname;
       val Name_Space {kind = k, internals, ...} = space;
       val ext = extern_shortest (Context.proof_of context) space;
       val names =

   let val name = intern space xname in
     (case Symtab.lookup tab name of
       SOME x =>
         let
           val reports =
-            if Context_Position.is_visible_generic context andalso Position.is_reported pos
+            if Context_Position.is_reported_generic context pos
             then [(pos, markup space name)] else [];
         in ((name, reports), x) end
     | NONE =>
         error (undefined (kind_of space) name ^ Position.here pos ^
           Markup.markup Markup.report