Closed
Description
In 1.4.0 we introduced completions for all the identifiers defined in the project. The database of possible identifiers is refreshed on every kick, as you type. This means new entries being added literally as you type, even if you hadn't finished typing yet :)
In the screenshot below, GarbageCollectDirtyKeys is a new constructor I have just defined a minute ago. I get completions for several prefixes of it. Ideally I only want to get only one completion for the full identifier:
How to prevent this? When refreshing the database of identifiers for a module M, wipe out all the previous entries of M in the database. This might require additional indexes.