--- a/src/Pure/General/name_space.ML Wed Mar 05 18:26:35 2014 +0100
+++ b/src/Pure/General/name_space.ML Wed Mar 05 19:52:28 2014 +0100
@@ -205,8 +205,7 @@
(* 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;
@@ -453,7 +452,7 @@
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 =>