Tracking PR for monaco #1
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
joneugster
force-pushed
the
monaco
branch
2 times, most recently
from
b1827b3 to
7273f20
Compare
joneugster
force-pushed
the
monaco
branch
4 times, most recently
from
0630089 to
33c2da0
Compare
I somehow reverted this by accident during testing. `1ch` of padding feels much more consistent for the unsolved goal symbol.
…r#589) The language client library has a very convenient setting for tracing language server messages on the client-side, but I'm getting tired of having to edit the `settings.json` to use it. This PR exposes the client-side logging setting in the vscode-lean4 config.
This PR makes the edit delay for the "unsolved goal" decoration adjustable for testing purposes, reduces it to 750ms and fixes a bug that caused the decoration to sometimes be displayed in the wrong location for a moment.
This PR allows theme colors in the color settings for the 'unsolved goals' decoration and changes the default color of the 'unsolved goals' decoration to `editorInfo.foreground`.
I’m not certain whether this is the best place to add a new `registerUriHandler`. However, it's a hook for the URI `vscode://leanprover.lean4/setup-guide`, which will open the setup guide. This is useful for future documentation in the web, especially when detailing the installation process.
…ipt ₈ conflict (leanprover#599) Rename the unused "8<" abbreviation as "scissor". This resolves the need for an extra space when typing "\8" to get ₈, and makes "\8" = ₈ work like all other subscript digits (e.g. "\0" = ₀, "\1" = ₁). "8<" is not used in Mathlib or Lean. Co-authored-by: euprunin <[email protected]>
This PR adjusts tests that check the contents of 'All Messages' to check the content of 'Messages' instead, which (when initializing the InfoView for the first time) is sometimes subject to a race condition that makes it not display any messages. This is a known, albeit minor, issue.
This PR improves the performance of the new editor decorations that were introduced in leanprover#585. Specifically, it makes the following adjustments: - The result of `workspace.getConfiguration` is cached. This VS Code API is slower than expected, so we can't call it for every single decoration. - The decoration debounce delay is increased. - The decoration debounce delay applies to 'unsolved goals' decorations as well. - The work to compute the decorations is slightly reduced.
This PR makes the following adjustments: - Fix a potential bug where nested workspace folders could lead to nested language servers (i.e. in core) - Improve error reporting for nested language servers - Improve error reporting for the 'Restart File' command
This PR prevents users from accidentally editing dependencies in `.lake` and `.elan` when jumping to them, e.g. using go-to-definition.
…oolchain (leanprover#610) This PR ensures that an error is displayed when users open a project that has a lakefile but no lean-toolchain file.
This PR ensures that the installed toolchains in all commands that display them are sorted in a sensible manner.
…anprover#613) Every so often, users decide that they want to get (what they believe to be) the "full" Lean experience in VS Code and install every single Lean-related extension from the VS Code marketplace. While well-intentioned, since the marketplace also contains forks of our extension, this then leads to an internal activation error when VS Code's `commands.registerCommand` API throws an exception for trying to register duplicate commands. This PR improves the error message that is displayed in this case to hint at the cause so that users are more likely to be able to fix it themselves without requiring assistance.
This PR revamps the option and action UX of the InfoView. This work is motivated by several reports from users that they never knew that certain InfoView functionality existed, and intends to make these features more discoverable. Closes leanprover#592. Specifically, the following adjustments are made: - The filter menu was difficult to discover and users had trouble finding the 'reverse tactic state' functionality. To improve this, all goal state settings have been moved into a single 'Settings' menu that uses a standard cog icon, which should hopefully be much more recognizable. - All goal state settings are now also available in the 'Settings' submenu of the InfoView context menu. - The 'Unselect All' context menu entry is now only visible when there is something to be unselected, as is the case for other context menu entries. - All goal state settings can be persisted to the VS Code user settings with a context menu action or a button in the settings menu. Clients that do not support this functionality can hide the button in the settings menu by hiding the elements with `saveConfigButton` and `saveConfigLineBreak` classes. - The `reverseTacticState`, `showGoalNames` and `emphasizeFirstGoal` settings have been made available in the InfoView goal state settings menu. - All InfoView actions have been made available in the context menu. - The 'Copy to comment' and 'Copy to clipboard' actions have been removed. As of [vscode#206529](microsoft/vscode#206529), copying from VS Code webviews should work correctly out-of-the-box, so there is no need for these additional buttons that may unnecessarily complicate the UI anymore. - The 'Refresh' action has been adjusted so that it is only displayed when the InfoView is paused to explicitly hint at the fact that it can be used to refresh the goal state while the InfoView is paused. Many users used to think that this was just the "Retry if InfoView is broken" button, which is practically never necessary. - The tooltips of all InfoView icons have been adjusted to be a bit more descriptive. - The `lean4.infoview.showExpectedType` setting has been deprecated in favor of the new `lean4.infoview.expectedTypeVisibility` setting, which allows hiding the expected type section entirely, as this section was reported to be confusing for students in a teaching environment. <details> <summary>Adjusted InfoView UI (Click to open)</summary>  </details> <details> <summary>New settings menu (Click to open)</summary>  </details> <details> <summary>New InfoView context menu (Click to open)</summary>  </details>
This PR ensures that the tooltip hover popup doesn't trigger while the primary mouse button is being held to prevent it from popping up while user are selecting text.
This PR fixes the fallout of a small ticking time bomb that exploded in v4.21.0-rc1. Lake reports its version strings as follows, where `77cfc4d` is the commit ID of the corresponding release: ``` [mhuisi@fedora ~]$ lake --version Lake version 5.0.0-77cfc4d (Lean version 4.20.0) ``` In v4.21.0-rc1, the commit ID is `0168680`, so Lake reports the following version string: ``` [mhuisi@fedora ~]$ lake --version Lake version 5.0.0-0168680 (Lean version 4.21.0-rc1) ``` Unfortunately, `5.0.0-0168680` is *not* a [valid semantic version](https://semver.org/), since it both contains a 0 at the start and only numbers. This is fairly rare, but it now happened on v4.21.0-rc1 for the first time. The VS Code extension parses this version as part of its precondition checks, which now fails because the version is not a valid semantic version. The workaround for this issue is to remove the step that parses the version. The extension only parsed it for consistency with other precondition checks and doesn't actually do anything interesting with the version, so removing it doesn't lose us anything.
This PR adjusts the progress bar message to reflect that it is cloning missing packages (suggesting that it may hence take a while). It also adjusts the output of `lake serve` in the output panel to mention the command that was called.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR keeps track of all modifications we'd like for using the
vscode-lean4with a monaco editor.merged:
Further, there is one small fix to deal with mismatching client/server OS, but I'm not sure this would be the right fix in the extension. Therefore it's merely here for reference:
Updating everything
Here are the steps to keep these PRs and the entire project up-to-date with
vscode-lean4:master. Ideally these are done from within the submodulelean4monaco/src/vscode-lean4:masterbranch with upstream (can be done here with the github UI)masterto a "Release" commit! This ensures no version clash with the published packages@leanprover/infoviewetc.masterand force-push.monacobranch. For example, reset it tomaster, then merge all branches listed here again (e.g. in the order provided).lean4monaconpm update @leanprover/infoviewinlean4monaco, too.lean4monacoto npm, and then callnpm update lean4monacoinlean4web.