# HG changeset patch
# User wenzelm
# Date 1394189291 -3600
# Node ID 9962ca0875c98313c0d557e76aa62f8a3cc03390
# Parent  c835a937902674af45be2afb9dea29bab1363189
no completion of concealed names;

diff -r c835a9379026 -r 9962ca0875c9 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Mar 07 11:46:26 2014 +0100
+++ b/src/Pure/General/name_space.ML	Fri Mar 07 11:48:11 2014 +0100
@@ -208,11 +208,13 @@
   if Position.is_reported pos then
     let
       val x = Name.clean xname;
-      val Name_Space {kind = k, internals, ...} = space;
+      val Name_Space {kind, internals, ...} = space;
       val ext = extern_shortest (Context.proof_of context) space;
       val names =
         Symtab.fold
-          (fn (a, (b :: _, _)) => String.isPrefix x a ? cons (ext b, Long_Name.implode [k, b])
+          (fn (a, (name :: _, _)) =>
+              if String.isPrefix x a andalso not (is_concealed space name)
+              then cons (ext name, Long_Name.implode [kind, name]) else I
             | _ => I) internals []
         |> sort_distinct (string_ord o pairself #1);
     in Completion.names pos names end