leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
158 stars 48 forks source link

fix: revert to using one abbreviation rewriter for active editor #480

Closed mhuisi closed 3 months ago

mhuisi commented 3 months ago

In #469, I refactored the abbreviation provider to maintain one abbreviation rewriter per visible text editor. The idea was that it would be nice if the abbreviation state was maintained when switching between visible text editors.

It turns out that this is way too fiddly to get right:

Still, the new behavior is a bit more consistent than the behavior before #469, as it correctly deals with changed language IDs and triggers abbreviations when moving the cursor away from the editor (instead of simply unselecting the abbreviation).

This PR also ensures that exceptions during the activation of the extension are displayed in a modal dialog. An exception at this point always breaks the extension for the user, so they should know about it (and the error shouldn't be hidden away in the developer console).

Fixes #478.