You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: