# HG changeset patch
# User wenzelm
# Date 1394134003 -3600
# Node ID c2d4a3608441c1969ab4f66ac7aa7319bddf597e
# Parent  beef468837b14f09c80603e00ffad23042517a96
completion is part of error (not report) and thus not subject to context visibility -- e.g. relevant for 'fixes' in long statements;

diff -r beef468837b1 -r c2d4a3608441 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Mar 06 19:55:08 2014 +0100
+++ b/src/Pure/General/name_space.ML	Thu Mar 06 20:26:43 2014 +0100
@@ -205,7 +205,7 @@
 (* completion *)
 
 fun completion context space (xname, pos) =
-  if Context_Position.is_reported_generic context pos then
+  if Position.is_reported pos then
     let
       val x = Name.clean xname;
       val Name_Space {kind = k, internals, ...} = space;