feat: revamp infoview options and actions (#606)

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](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>

![Adjusted InfoView
UI](https://github.com/user-attachments/assets/3988695f-ff5b-4355-92fa-fdd62aae6cae)

</details>

<details>
<summary>New settings menu (Click to open)</summary>

![New settings
menu](https://github.com/user-attachments/assets/14721d72-f9c3-423e-a642-40a1e12348a6)

</details>

<details>
<summary>New InfoView context menu (Click to open)</summary>

![New InfoView context
menu](https://github.com/user-attachments/assets/e7b7b129-b74a-40f9-9fd6-63db2d4bba5e)

</details>

Author: mhuisi

lean4-infoview-api/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview-api",
-    "version": "0.6.0",
+    "version": "0.7.0",
     "description": "Types and API for @leanprover/infoview.",
     "scripts": {
         "watch": "tsc --watch",

lean4-infoview-api/src/infoviewApi.ts

@@ -7,6 +7,23 @@ import type {
     WorkspaceEdit,
 } from 'vscode-languageserver-protocol'
 
+export type ExpectedTypeVisibility = 'Expanded by default' | 'Collapsed by default' | 'Hidden'
+
+export interface InfoviewConfig {
+    allErrorsOnLine: boolean
+    autoOpenShowsGoal: boolean
+    debounceTime: number
+    expectedTypeVisibility: ExpectedTypeVisibility
+    showGoalNames: boolean
+    emphasizeFirstGoal: boolean
+    reverseTacticState: boolean
+    hideTypeAssumptions: boolean
+    hideInstanceAssumptions: boolean
+    hideInaccessibleAssumptions: boolean
+    hideLetValues: boolean
+    showTooltipOnHover: boolean
+}
+
 /**
  * An insert `here` should be written exactly at the specified position,
  * while one `above` should go on the preceding line.
@@ -15,6 +32,8 @@ export type TextInsertKind = 'here' | 'above'
 
 /** Interface that the InfoView WebView uses to talk to the hosting editor. */
 export interface EditorApi {
+    saveConfig(config: InfoviewConfig): Promise<any>
+
     /** Make a request to the LSP server. */
     sendClientRequest(uri: string, method: string, params: any): Promise<any>
     /** Send a notification to the LSP server. */
@@ -77,25 +96,18 @@ export interface InfoviewTacticStateFilter {
     flags: string
 }
 
-export interface InfoviewConfig {
-    allErrorsOnLine: boolean
-    autoOpenShowsGoal: boolean
-    debounceTime: number
-    showExpectedType: boolean
-    showGoalNames: boolean
-    emphasizeFirstGoal: boolean
-    reverseTacticState: boolean
-    showTooltipOnHover: boolean
-}
-
 export const defaultInfoviewConfig: InfoviewConfig = {
     allErrorsOnLine: true,
     autoOpenShowsGoal: true,
     debounceTime: 50,
-    showExpectedType: true,
+    expectedTypeVisibility: 'Expanded by default',
     showGoalNames: true,
     emphasizeFirstGoal: false,
     reverseTacticState: false,
+    hideTypeAssumptions: false,
+    hideInstanceAssumptions: false,
+    hideInaccessibleAssumptions: false,
+    hideLetValues: false,
     showTooltipOnHover: true,
 }
 
@@ -108,7 +120,35 @@ export type InfoviewActionKind =
 
 export type InfoviewAction = { kind: InfoviewActionKind }
 
-export type ContextMenuEntry = 'goToDefinition' | 'select' | 'unselect' | 'unselectAll'
+export type ContextMenuEntry =
+    | 'goToDefinition'
+    | 'select'
+    | 'unselect'
+    | 'unselectAll'
+    | 'pause'
+    | 'unpause'
+    | 'pin'
+    | 'unpin'
+    | 'refresh'
+    | 'pauseAllMessages'
+    | 'unpauseAllMessages'
+    | 'goToPinnedLocation'
+    | 'goToMessageLocation'
+    | 'displayTargetBeforeAssumptions'
+    | 'displayAssumptionsBeforeTarget'
+    | 'hideTypeAssumptions'
+    | 'showTypeAssumptions'
+    | 'hideInstanceAssumptions'
+    | 'showInstanceAssumptions'
+    | 'hideInaccessibleAssumptions'
+    | 'showInaccessibleAssumptions'
+    | 'hideLetValues'
+    | 'showLetValues'
+    | 'hideGoalNames'
+    | 'showGoalNames'
+    | 'emphasizeFirstGoal'
+    | 'deemphasizeFirstGoal'
+    | 'saveSettings'
 
 export interface ContextMenuAction {
     entry: ContextMenuEntry

lean4-infoview/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview",
-    "version": "0.8.3",
+    "version": "0.8.4",
     "description": "An interactive display for the Lean 4 theorem prover.",
     "scripts": {
         "watch": "rollup --config --environment NODE_ENV:development --watch",
@@ -49,7 +49,7 @@
         "typescript": "^5.4.5"
     },
     "dependencies": {
-        "@leanprover/infoview-api": "~0.6.0",
+        "@leanprover/infoview-api": "~0.7.0",
         "@vscode/codicons": "^0.0.32",
         "@vscode-elements/react-elements": "^0.5.0",
         "es-module-lexer": "^1.5.4",

lean4-infoview/src/infoview/collapsing.tsx

@@ -26,19 +26,24 @@ export function useIsVisible(): [(element: HTMLElement) => void, boolean] {
     return [node, isVisible]
 }
 
-interface DetailsProps {
+interface DetailsProps extends React.PropsWithoutRef<React.HTMLProps<HTMLDetailsElement>> {
     initiallyOpen?: boolean
     children: [React.ReactNode, ...React.ReactNode[]]
     setOpenRef?: (_: React.Dispatch<React.SetStateAction<boolean>>) => void
 }
 
 /** Like `<details>` but can be programatically revealed using `setOpenRef`.
  * The first child is placed inside the `<summary>` node. */
-export function Details({ initiallyOpen, children: [summary, ...children], setOpenRef }: DetailsProps): JSX.Element {
+export function Details({
+    initiallyOpen,
+    children: [summary, ...children],
+    setOpenRef,
+    ...props
+}: DetailsProps): JSX.Element {
     const [isOpen, setOpen] = React.useState<boolean>(initiallyOpen === undefined ? false : initiallyOpen)
     if (setOpenRef) setOpenRef(setOpen)
     return (
-        <details open={isOpen}>
+        <details open={isOpen} {...props}>
             <summary
                 className="mv2 pointer "
                 onClick={e => {