v0.0.125

• Mitigate two race conditions in the abbreviation provider (#389) that made the cursor jump to the wrong location when completing an abbreviation and would sometimes issue an "Unable to replace abbreviation" error, especially with increased latency.

v0.0.124

• Make word-based occurrence highlighting fallback optional and set the default to disable it, c.f. #377 (Author: @david-christiansen)
• Make InfoView colors configurable (Author: @david-christiansen)
• Allow downloading projects with SSH Git links
• Add the following abbreviations: average: ⨍, -int: ⨍, oiint: ∯, tint: ∯, pd: ∂ (Author: @girving)
• Add red syntactic highlighting for sorry-like identifiers (admit, stop)
• Display a modal warning before updating in the 'Update Dependency' command
• Change label of 'Rebuild Imports' to 'Restart File' so that it is clear that they are the same thing
• Adjust setup guide to move the description of what Lean depends on to the front

v0.0.122

• Add language client support for snippets in text edits, enabling the use of snippets in code actions and widgets (c.f. leanprover/lean4#3054)
• Make user widget names optional now that user-widgets have been generalized to non-top-level widget declarations (c.f. leanprover/lean4#2963)

v0.0.121

• Try to fix a bug where the setup guide would not open after installing the extension.
  • The bug still seems to be present in the released version.

v0.0.120

• Update the setup guide to be more detailed and include information on VS Code extension features that do not immediately present themselves to users
• Build standalone Lean projects after initialization so that users do not get an "imports outdated" error immediately after
• Change scope ID of Lean's markdown grammar so that it doesn't conflict with that of the Lean 3 extension
• Add \rrbracket to list of abbreviations

v0.0.119

• When using the "Update Dependency" command, update the lean-toolchain after running lake update. Since Mathlib may now update the lean-toolchain by itself during lake update, this order is causing fewer problems.
• Add compatibility for new Lake manifest version so that "Update Dependency" works with v4.3.0-rc2.
• Rename "Install Lean using Elan" button to just "Install Lean" to reduce confusion about Elan
• Fix bug where Lean language client wouldn't start if the project folder was detected as invalid

v0.0.118

• Remove the server restart prompt after discussion on Zulip
• Change name of lean4.createMathlibProject to be easier to understand
• Ensure that "Restart File" (Ctrl+Shift+X) does not open the extensions menu anymore when in a Lean 4 context
• Make "Toggle Infoview" and "Toggle All Messages" keybindings work when not focusing the editor window
• Ensure that commands displayed in command pallette are independent of focused part of VS Code
• Fix Lean server crashing with bad error message when no default toolchain is set because it was uninstalled in the past

v0.0.117

• Add project commands, command menu and walkthrough (#334)
• Change defaults for whitespace settings in Lean 4 files (#341)

v0.0.116-pre

(Pre-Release)

• Add project commands, command menu and walkthrough (#334)

v0.0.113

• Add notification that is displayed when the server reports that the imports are out of date