Skip to content

Releases: leanprover/vscode-lean4

v0.0.236

28 Apr 08:01

Choose a tag to compare

  • Add three new abbreviation-related commands that have the goal of making it easier to insert Unicode symbols into non-editor dialogs and to make abbreviations more discoverable (#762):
    • 'Find Unicode Symbol...': Displays a picker dialog that allows searching for Unicode symbols either by abbreviation or by symbol. Selecting an entry then provides an option to either copy the symbol or to insert it into the currently active text editor. Displayed in the forall menu.
    • 'Copy Unicode Symbol...': Like 'Find Unicode Symbol', but selecting a symbol from the dialog immediately copies it instead of opening another dialog to choose whether the symbol should be inserted or copied. Bound to Ctrl+Alt+\ when no text editor is focused.
    • 'Insert Unicode Symbol...': Like 'Find Unicode Symbol', but selecting a symbol from the dialog immediately inserts it instead of opening another dialog to choose whether the symbol should be inserted or copied. Bound to Ctrl+Alt+\ when a text editor is focused.
  • Implement client-side support for planned incremental diagnostic support in the language server (#752)
  • Fix a bug where the extension would not correctly apply code action snippet edits (#777, author: @Vtec234)
  • Replace the Lean file icon with the forall icon (#767)
  • Remove three abbreviations that produce unicode symbols that Mathlib lints against (#764)
  • Remove HTML highlighting from the Markdown syntax highlighting in Lean doc comments (#770)
  • Fix a bug where the abbreviation for would not trigger correctly (#775)
  • Fix a bug where the Markdown grammar of Lean incorrectly highlighted code after a doc comment (#773)

v0.0.235-pre

15 Apr 09:12

Choose a tag to compare

v0.0.235-pre Pre-release
Pre-release
  • Add three new abbreviation-related commands that have the goal of making it easier to insert Unicode symbols into non-editor dialogs and to make abbreviations more discoverable (#762):
    • 'Find Unicode Symbol...': Displays a picker dialog that allows searching for Unicode symbols either by abbreviation or by symbol. Selecting an entry then provides an option to either copy the symbol or to insert it into the currently active text editor. Displayed in the forall menu.
    • 'Copy Unicode Symbol...': Like 'Find Unicode Symbol', but selecting a symbol from the dialog immediately copies it instead of opening another dialog to choose whether the symbol should be inserted or copied. Bound to Ctrl+Alt+\ when no text editor is focused.
    • 'Insert Unicode Symbol...': Like 'Find Unicode Symbol', but selecting a symbol from the dialog immediately inserts it instead of opening another dialog to choose whether the symbol should be inserted or copied. Bound to Ctrl+Alt+\ when a text editor is focused.
  • Implement client-side support for planned incremental diagnostic support in the language server (#752)
  • Replace the Lean file icon with the forall icon (#767)
  • Remove three abbreviations that produce unicode symbols that Mathlib lints against (#764)

v0.0.234

13 Apr 12:38

Choose a tag to compare

  • Split the 'Fetch Mathlib Build Cache For Current Imports' command into three (#757)
  • Ensure that 'Fetch Mathlib Build Cache For ...' commands can be used downstream of Mathlib (#757)
  • Add file icons for .lean files (#749, #753)
  • Ensure that redundant redundant interactive requests are canceled (#746, author: @Vtec234)
  • Fix a bug where some commands would sometimes try to execute in the wrong project (#750)
  • Fix a potential bug where closing the InfoView could yield an 'undefined' error (#756)
  • Improve progress bar messages when downloading a project (#748)

v0.0.233-pre

09 Apr 08:17

Choose a tag to compare

v0.0.233-pre Pre-release
Pre-release
  • Split the 'Fetch Mathlib Build Cache For Current Imports' command into three (#757)
  • Ensure that 'Fetch Mathlib Build Cache For ...' commands can be used downstream of Mathlib (#757)

v0.0.232-pre

07 Apr 07:59

Choose a tag to compare

v0.0.232-pre Pre-release
Pre-release
  • Fix a potential bug where closing the InfoView could yield an 'undefined' error (#756)

v0.0.231-pre

02 Apr 08:21

Choose a tag to compare

v0.0.231-pre Pre-release
Pre-release
  • Swap light and dark Lean language file icons (#753)

v0.0.230-pre

01 Apr 08:06

Choose a tag to compare

v0.0.230-pre Pre-release
Pre-release
  • Ensure that redundant redundant interactive requests are canceled (#746, author: @Vtec234)
  • Fix a bug where some commands would sometimes try to execute in the wrong project (#750)
  • Add file icons for .lean files (#749)
  • Improve progress bar messages when downloading a project (#748)

v0.0.229

31 Mar 09:44

Choose a tag to compare

  • Ensure that Git is correctly added to process PATH during installation on systems where winget installs it to %LocalAppData% (#744)
  • Make Git installation on Windows via winget more robust against SSL tampering (#743)

v0.0.228-pre

25 Mar 07:51

Choose a tag to compare

v0.0.228-pre Pre-release
Pre-release
  • Ensure that Git is correctly added to process PATH during installation on systems where winget installs it to %LocalAppData% (#744)

v0.0.227-pre

24 Mar 14:45

Choose a tag to compare

v0.0.227-pre Pre-release
Pre-release
  • Make Git installation on Windows via winget more robust against SSL tampering (#743)