src/Pure/General/name_space.ML
changeset 55923 4bdae9403baf
parent 55922 710bc66f432c
child 55956 94d384d621b0
equal deleted inserted replaced
55922:710bc66f432c 55923:4bdae9403baf
   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 Context_Position.is_visible_generic context andalso Position.is_reported pos
   208   if Context_Position.is_reported_generic context pos then
   209   then
       
   210     let
   209     let
   211       val x = Name.clean xname;
   210       val x = Name.clean xname;
   212       val Name_Space {kind = k, internals, ...} = space;
   211       val Name_Space {kind = k, internals, ...} = space;
   213       val ext = extern_shortest (Context.proof_of context) space;
   212       val ext = extern_shortest (Context.proof_of context) space;
   214       val names =
   213       val names =
   451   let val name = intern space xname in
   450   let val name = intern space xname in
   452     (case Symtab.lookup tab name of
   451     (case Symtab.lookup tab name of
   453       SOME x =>
   452       SOME x =>
   454         let
   453         let
   455           val reports =
   454           val reports =
   456             if Context_Position.is_visible_generic context andalso Position.is_reported pos
   455             if Context_Position.is_reported_generic context pos
   457             then [(pos, markup space name)] else [];
   456             then [(pos, markup space name)] else [];
   458         in ((name, reports), x) end
   457         in ((name, reports), x) end
   459     | NONE =>
   458     | NONE =>
   460         error (undefined (kind_of space) name ^ Position.here pos ^
   459         error (undefined (kind_of space) name ^ Position.here pos ^
   461           Markup.markup Markup.report
   460           Markup.markup Markup.report