This fixes an issue introduced in the abbreviation refactor of #469 that would sometimes cause the extension to not activate properly because a command was attempted to be registered multiple times. It also fixes another bug where Tab completion did not work correctly in non-Lean 4 files.
This fixes an issue introduced in the abbreviation refactor of #469 that would sometimes cause the extension to not activate properly because a command was attempted to be registered multiple times. It also fixes another bug where
Tabcompletion did not work correctly in non-Lean 4 files.Fixes #475.