src/Pure/General/name_space.ML
changeset 55845 a05413276a0d
parent 55840 2982d233d798
child 55922 710bc66f432c
equal deleted inserted replaced
55844:fc04c24ad9ee 55845:a05413276a0d
   204 
   204 
   205 fun completion context space (xname, pos) =
   205 fun completion context space (xname, pos) =
   206   if Context_Position.is_visible_generic context andalso Position.is_reported pos
   206   if Context_Position.is_visible_generic context andalso Position.is_reported pos
   207   then
   207   then
   208     let
   208     let
       
   209       val x = Name.clean xname;
   209       val Name_Space {kind = k, internals, ...} = space;
   210       val Name_Space {kind = k, internals, ...} = space;
   210       val ext = extern_shortest (Context.proof_of context) space;
   211       val ext = extern_shortest (Context.proof_of context) space;
   211       val names =
   212       val names =
   212         Symtab.fold
   213         Symtab.fold
   213           (fn (a, (b :: _, _)) => String.isPrefix xname a ? cons (ext b, Long_Name.implode [k, b])
   214           (fn (a, (b :: _, _)) => String.isPrefix x a ? cons (ext b, Long_Name.implode [k, b])
   214             | _ => I) internals []
   215             | _ => I) internals []
   215         |> sort_distinct (string_ord o pairself #1);
   216         |> sort_distinct (string_ord o pairself #1);
   216     in Completion.names pos names end
   217     in Completion.names pos names end
   217   else Completion.none;
   218   else Completion.none;
   218 
   219