Skip to content

feat: revamp infoview options and actions#606

Merged
mhuisi merged 6 commits intomasterfrom
mhuisi/infoview-ux
Apr 23, 2025
Merged

feat: revamp infoview options and actions#606
mhuisi merged 6 commits intomasterfrom
mhuisi/infoview-ux

Conversation

@mhuisi
Copy link
Copy Markdown
Collaborator

@mhuisi mhuisi commented Apr 11, 2025

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 #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, 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.
Adjusted InfoView UI (Click to open)

Adjusted InfoView UI

New settings menu (Click to open)

New settings menu

New InfoView context menu (Click to open)

New InfoView context menu

Copy link
Copy Markdown
Member

@Vtec234 Vtec234 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have not looked at the implementation at all, but everything seems to work when tested locally.

@mhuisi mhuisi merged commit 8e34c2e into master Apr 23, 2025
2 checks passed
@ctchou
Copy link
Copy Markdown

ctchou commented Apr 29, 2025

Why were the 'Copy to comment' and 'Copy to clipboard' actions removed without any announcement or discussion in the Lean community Zulip? I used those features often and was dismayed that they just suddenly disappeared.

mhuisi added a commit that referenced this pull request Aug 14, 2025
This PR re-adds the copy state/message to clipboard functionality after
it was removed in #606. The functionality is available from the context
menu (as the other "edit" webview actions are), not from an icon button.
@mhuisi mhuisi deleted the mhuisi/infoview-ux branch October 21, 2025 12:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Improve discoverability of InfoView settings and actions

3 participants