src/Pure/General/name_space.ML
changeset 55989 55827fc7c0dd
parent 55977 ec4830499634
child 56022 8c9ab5d91d5a
equal deleted inserted replaced
55988:ffe88d72afae 55989:55827fc7c0dd
   203 
   203 
   204 
   204 
   205 (* completion *)
   205 (* completion *)
   206 
   206 
   207 fun completion context space (xname, pos) =
   207 fun completion context space (xname, pos) =
   208   if Position.is_reported pos then
   208   if Position.is_reported pos andalso xname <> "" andalso xname <> "_" then
   209     let
   209     let
   210       val x = Name.clean xname;
   210       val x = Name.clean xname;
   211       val Name_Space {kind, internals, ...} = space;
   211       val Name_Space {kind, internals, ...} = space;
   212       val ext = extern_shortest (Context.proof_of context) space;
   212       val ext = extern_shortest (Context.proof_of context) space;
   213       val names =
   213       val names =