Infoview tweaks

README.md

@@ -201,6 +201,14 @@ name of the relative path to the store the logs.
 
 * `lean4.infoview.debounceTime`: how long (in milliseconds) the infoview waits before displaying new information after the cursor has stopped moving. The optimal value depends on your machine - try experimenting. The default is `50`.
 
+* `lean4.infoview.showExpectedType`: show the expected type by default. This display can then be toggled by clicking on the title or using the <kbd>Ctrl</kbd>+<kbd>Alt</kbd>+<kbd>e</kbd> `Lean 4: Infoview: Show Expected Type` command. The default is `true`.
+
+* `lean4.infoview.showGoalNames`: show goal names (e.g. `case inl` in the infoview). The default is `true`.
+
+* `lean4.infoview.emphasizeFirstGoal`: emphasize the first goal by displaying the other goals with reduced size and opacity. The default is `false`.
+
+* `lean4.infoview.reverseTacticState`: show each goal above its local context by default. This can also be toggled by clicking a button (see the Infoview panel description above). The default is `false`.
+
 ## Extension commands
 
 This extension also contributes the following commands, which can be bound to keys if desired using the [VS Code keyboard bindings](https://code.visualstudio.com/docs/getstarted/keybindings).
@@ -240,6 +248,8 @@ the server for the file needs to be restarted to pick up the changed dependency.
 
 * `lean4.infoView.toggleUpdating` (Lean 4: Infoview: Toggle Updating): pause / continue live updates of the main (unpinned) tactic state widget (same as clicking on the <img height="16" src="vscode-lean4/media/pause.png"/> or <img height="16" src="vscode-lean4/media/continue.png"/> icon on the main tactic state widget.)
 
+* `lean4.infoView.toggleExpectedType` (Lean 4: Infoview: Toggle Expected Type): toggles the "Expected Type" widget in the Infoview (bound to <kbd>ctrl</kbd>+<kbd>alt</kbd>+<kbd>e</kbd> by default)
+
 ### Documentation commands
 
 * `lean4.docView.open` (Lean 4: Open Documentation View): Open documentation found in local 'html' folder in a separate web view panel.

lean4-infoview-api/src/infoviewApi.ts

@@ -79,19 +79,26 @@ export interface InfoviewConfig {
     allErrorsOnLine: boolean;
     autoOpenShowsGoal: boolean;
     debounceTime: number;
+    showExpectedType: boolean;
+    showGoalNames: boolean;
+    emphasizeFirstGoal: boolean;
+    reverseTacticState: boolean;
 }
 
 export const defaultInfoviewConfig: InfoviewConfig = {
     allErrorsOnLine: true,
     autoOpenShowsGoal: true,
     debounceTime: 50,
+    showExpectedType: true,
+    showGoalNames: true,
+    emphasizeFirstGoal: false,
+    reverseTacticState: false,
 }
 
-export type InfoviewAction =
-  { kind: 'toggleAllMessages'} |
-  { kind: 'togglePaused' } |
-  { kind: 'togglePin'} |
-  { kind: 'copyToComment'}
+export type InfoviewActionKind =
+  'toggleAllMessages' | 'togglePaused' | 'togglePin' | 'copyToComment' | 'toggleExpectedType'
+
+export type InfoviewAction = { kind: InfoviewActionKind }
 
 /** Interface the hosting editor uses to talk to the InfoView WebView. */
 export interface InfoviewApi {

lean4-infoview/src/infoview/collapsing.tsx

@@ -26,7 +26,7 @@ export function useIsVisible(): [(element: HTMLElement) => void, boolean] {
 interface DetailsProps {
     initiallyOpen?: boolean;
     children: [React.ReactNode, ...React.ReactNode[]];
-    setOpenRef?: React.MutableRefObject<React.Dispatch<React.SetStateAction<boolean>>>;
+    setOpenRef?: (_: React.Dispatch<React.SetStateAction<boolean>>) => void;
 }
 
 /** Like `<details>` but can be programatically revealed using `setOpenRef`. */
@@ -37,9 +37,8 @@ export function Details({initiallyOpen, children: [summary, ...children], setOpe
             node.addEventListener('toggle', () => setOpen(node.open));
         }
     }, []);
-    if (setOpenRef) setOpenRef.current = setOpen;
-    /* HACK: `as any` works around a bug in `@types/react` */
-    return <details ref={setupEventListener as any} open={isOpen}>
+    if (setOpenRef) setOpenRef(setOpen);
+    return <details ref={setupEventListener} open={isOpen}>
         {summary}
         { isOpen && children }
     </details>;

lean4-infoview/src/infoview/goals.tsx

@@ -1,9 +1,13 @@
 import * as React from 'react'
 import { InteractiveCode } from './interactiveCode'
-import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle, InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api'
+import { InfoviewActionKind, InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle,
+    InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags }
+    from '@leanprover/infoview-api'
 import { WithTooltipOnHover } from './tooltips';
-import { EditorContext } from './contexts';
+import { EditorContext, ConfigContext } from './contexts';
 import { Locations, LocationsContext, SelectableLocation } from './goalLocation';
+import { Details } from './collapsing';
+import { useEvent } from './util';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
@@ -111,13 +115,15 @@ function Hyp({ hyp: h, mvarId }: HypProps) {
 interface GoalProps {
     goal: InteractiveGoal
     filter: GoalFilterState
+    additionalClassNames: string
 }
 
 /**
  * Displays the hypotheses, target type and optional case label of a goal according to the
  * provided `filter`. */
 export const Goal = React.memo((props: GoalProps) => {
-    const { goal, filter } = props
+    const { goal, filter, additionalClassNames } = props
+    const config = React.useContext(ConfigContext)
 
     const prefix = goal.goalPrefix ?? '⊢ '
     const filteredList = getFilteredHypotheses(goal.hyps, filter);
@@ -135,41 +141,51 @@ export const Goal = React.memo((props: GoalProps) => {
         </LocationsContext.Provider>
     </div>
 
-    let cn = 'font-code tl pre-wrap bl bw1 pl1 b--transparent '
-    if (props.goal.isInserted) cn += 'b--inserted '
-    if (props.goal.isRemoved) cn += 'b--removed '
+    let cn = 'font-code tl pre-wrap bl bw1 pl1 b--transparent mb3 ' + additionalClassNames
+    if (props.goal.isInserted) cn += ' b--inserted '
+    if (props.goal.isRemoved) cn += ' b--removed '
 
-    if (goal.userName) {
+    const children: React.ReactNode[] = [
+        filter.reverse && goalLi,
+        hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />),
+        !filter.reverse && goalLi
+    ]
+
+    if (goal.userName && config.showGoalNames) {
         return <details open className={cn}>
             <summary className='mv1 pointer'>
                 <strong className="goal-case">case </strong>{goal.userName}
             </summary>
-            {filter.reverse && goalLi}
-            {hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
-            {!filter.reverse && goalLi}
+            {children}
         </details>
     } else return <div className={cn}>
-        {filter.reverse && goalLi}
-        {hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
-        {!filter.reverse && goalLi}
+        {children}
     </div>
 })
 
 interface GoalsProps {
     goals: InteractiveGoals
     filter: GoalFilterState
+    /** Whether or not to display the number of goals. */
     displayCount: boolean
 }
 
-function Goals({ goals, filter, displayCount}: GoalsProps) {
+function Goals({ goals, filter, displayCount }: GoalsProps) {
     const nGoals = goals.goals.length
     if (nGoals === 0) {
         return <strong className="db2 mb2 goal-goals">No goals</strong>
     } else {
+        const config = React.useContext(ConfigContext)
+        const unemphasizeCn = 'o-70 font-size-code-smaller'
         return <>
             {displayCount &&
                 <strong className="db mb2 goal-goals">{nGoals} {1 < nGoals ? 'goals' : 'goal'}</strong>}
-            {goals.goals.map((g, i) => <Goal key={i} goal={g} filter={filter} />)}
+            {goals.goals.map((g, i) =>
+                <Goal
+                    key={i}
+                    goal={g}
+                    filter={filter}
+                    additionalClassNames={(i !== 0 && config.emphasizeFirstGoal) ? unemphasizeCn : ''}/>)}
         </>
     }
 }
@@ -183,15 +199,21 @@ interface FilteredGoalsProps {
      * settings and collapsed state will be as before. */
     goals?: InteractiveGoals
     /** Whether or not to display the number of goals. */
-    displayCount?: boolean
+    displayCount: boolean
+    /** Whether the list of goals should be expanded on first render. */
+    initiallyOpen: boolean
+    /** If specified, the display will be toggled (collapsed/expanded) when this action is requested
+     * by the user. */
+    togglingAction?: InfoviewActionKind
 }
 
 /**
  * Display goals together with a header containing the provided children as well as buttons
  * to control how the goals are displayed.
  */
-export const FilteredGoals = React.memo(({ headerChildren, goals, displayCount }: FilteredGoalsProps) => {
+export const FilteredGoals = React.memo(({ headerChildren, goals, displayCount, initiallyOpen, togglingAction }: FilteredGoalsProps) => {
     const ec = React.useContext(EditorContext)
+    const config = React.useContext(ConfigContext)
 
     const copyToCommentButton =
         <a className="link pointer mh2 dim codicon codicon-quote"
@@ -203,8 +225,7 @@ export const FilteredGoals = React.memo(({ headerChildren, goals, displayCount }
             title="copy state to comment" />
 
     const [goalFilters, setGoalFilters] = React.useState<GoalFilterState>(
-        { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true });
-
+        { reverse: config.reverseTacticState, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true });
     const sortClasses = 'link pointer mh2 dim codicon ' + (goalFilters.reverse ? 'codicon-arrow-up ' : 'codicon-arrow-down ');
     const sortButton =
         <a className={sortClasses} title="reverse list"
@@ -231,15 +252,22 @@ export const FilteredGoals = React.memo(({ headerChildren, goals, displayCount }
             <a className={'link pointer mh2 dim codicon ' + (isFiltered ? 'codicon-filter-filled ': 'codicon-filter ')}/>
         </WithTooltipOnHover>
 
+    const setOpenRef = React.useRef<React.Dispatch<React.SetStateAction<boolean>>>()
+    useEvent(ec.events.requestedAction, act => {
+        if (act.kind === togglingAction && setOpenRef.current !== undefined) {
+            setOpenRef.current(t => !t)
+        }
+    })
+
     return <div style={{display: goals !== undefined ? 'block' : 'none'}}>
-        <details open>
+        <Details setOpenRef={r => setOpenRef.current = r} initiallyOpen={initiallyOpen}>
             <summary className='mv2 pointer'>
                 {headerChildren}
                 <span className='fr'>{copyToCommentButton}{sortButton}{filterButton}</span>
             </summary>
             <div className='ml1'>
-                {goals && <Goals goals={goals} filter={goalFilters} displayCount={displayCount||false}></Goals>}
+                {goals && <Goals goals={goals} filter={goalFilters} displayCount={displayCount}></Goals>}
             </div>
-        </details>
+        </Details>
     </div>
 })

lean4-infoview/src/infoview/index.css

@@ -13,6 +13,11 @@ html,body {
     line-height: var(--vscode-editor-line-height);
 }
 
+.font-size-code-smaller {
+    font-size: calc(.8*var(--vscode-editor-font-size));
+    line-height: calc(.8*var(--vscode-editor-line-height));
+}
+
 .font-normal {
     font-family: var(--vscode-font-family);
     font-weight: var(--vscode-font-weight);

lean4-infoview/src/infoview/info.tsx

@@ -87,6 +87,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
     const hasWidget = userWidgets.length > 0;
     const hasError = !!error;
     const hasMessages = messages.length !== 0;
+    const config = React.useContext(ConfigContext)
 
     const nothingToShow = !hasError && !goals && !termGoal && !hasMessages && !hasWidget;
 
@@ -115,10 +116,20 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                 <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again.</a>
             </div>}
         <LocationsContext.Provider value={locs}>
-            <FilteredGoals headerChildren='Tactic state' key='goals' goals={goals} displayCount={true} />
+            <FilteredGoals
+                key='goals'
+                headerChildren='Tactic state'
+                initiallyOpen
+                goals={goals}
+                displayCount />
         </LocationsContext.Provider>
-        <FilteredGoals headerChildren='Expected type' key='term-goal'
-            goals={termGoal !== undefined ? {goals: [termGoal]} : undefined} />
+        <FilteredGoals
+            key='term-goal'
+            headerChildren='Expected type'
+            goals={termGoal !== undefined ? {goals: [termGoal]} : undefined}
+            initiallyOpen={config.showExpectedType}
+            displayCount={false}
+            togglingAction='toggleExpectedType' />
         {userWidgets.map(widget =>
             <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
                 <summary className='mv2 pointer'>{widget.name}</summary>

lean4-infoview/src/infoview/messages.tsx

@@ -129,7 +129,7 @@ export function AllMessages({uri: uri0}: { uri: DocumentUri }) {
 
     return (
     <RpcContext.Provider value={rs}>
-    <Details setOpenRef={setOpenRef as any} initiallyOpen={!config.autoOpenShowsGoal}>
+    <Details setOpenRef={r => setOpenRef.current = r} initiallyOpen={!config.autoOpenShowsGoal}>
         <summary className="mv2 pointer">
             All Messages ({diags.length})
             <span className="fr">

lean4-infoview/src/infoview/traceExplorer.tsx

@@ -113,7 +113,10 @@ function InteractiveMessageTag({tag: embed}: InteractiveTagProps<MsgEmbed>): JSX
     if ('expr' in embed)
         return <InteractiveCode fmt={embed.expr} />
     else if ('goal' in embed)
-        return <Goal goal={embed.goal} filter={{reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true}} />
+        return <Goal
+            goal={embed.goal}
+            filter={{reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true}}
+            additionalClassNames='' />
     else if ('lazyTrace' in embed)
         return <LazyTrace col={embed.lazyTrace[0]} cls={embed.lazyTrace[1]} msg={embed.lazyTrace[2]} />
     else if ('trace' in embed)

vscode-lean4/package.json

@@ -145,6 +145,26 @@
 					"default": "",
 					"markdownDescription": "Add an additional CSS snippet to the infoview."
 				},
+				"lean4.infoview.showExpectedType": {
+					"type": "boolean",
+					"default": true,
+					"markdownDescription": "Show the expected type by default."
+				},
+				"lean4.infoview.showGoalNames": {
+					"type": "boolean",
+					"default": true,
+					"markdownDescription": "Show goal names (e.g. `case inl`) in the infoview."
+				},
+				"lean4.infoview.emphasizeFirstGoal": {
+					"type": "boolean",
+					"default": false,
+					"markdownDescription": "Display goals other than the main goal in a smaller font size."
+				},
+				"lean4.infoview.reverseTacticState": {
+					"type": "boolean",
+					"default": false,
+					"markdownDescription": "Default to showing the goal type first and then the local context."
+				},
 				"lean4.elaborationDelay": {
 					"type": "number",
 					"default": 200,
@@ -203,13 +223,13 @@
 				"command": "lean4.displayList",
 				"category": "Lean 4",
 				"title": "Infoview: Toggle \"All Messages\"",
-				"description": "Toggles the \"All Messages\" widget in the infoview."
+				"description": "Toggles the \"All Messages\" panel in the infoview."
 			},
 			{
 				"command": "lean4.infoView.copyToComment",
 				"category": "Lean 4",
 				"title": "Infoview: Copy Contents to Comment",
-				"description": "Copy the contents of the currently active tactic state widget to a new comment on the previous line.",
+				"description": "Copy the contents of the currently active tactic state panel to a new comment on the previous line.",
 				"icon": {
 					"dark": "./media/copy-to-comment-dark.svg",
 					"light": "./media/copy-to-comment-light.svg"
@@ -219,18 +239,20 @@
 				"command": "lean4.infoView.toggleStickyPosition",
 				"category": "Lean 4",
 				"title": "Infoview: Toggle Pin",
-				"description": "Create or remove a tactic state widget pinned to show the goal at the current position.",
-				"icon": {
-					"dark": "./media/toggle-sticky-position-dark.svg",
-					"light": "./media/toggle-sticky-position-light.svg"
-				}
+				"description": "Create or remove a tactic state panel pinned to show the goal at the current position."
 			},
 			{
 				"command": "lean4.infoView.toggleUpdating",
 				"category": "Lean 4",
 				"title": "Infoview: Toggle Updating",
 				"description": "Pause / Continue live updating of the main tactic state widget."
 			},
+			{
+				"command": "lean4.infoView.toggleExpectedType",
+				"category": "Lean 4",
+				"title": "Infoview: Toggle Expected Type",
+				"description": "Toggle the display of expected type."
+			},
 			{
 				"command": "lean4.docView.showAllAbbreviations",
 				"category": "Lean 4",
@@ -241,7 +263,7 @@
 				"command": "lean4.docView.open",
 				"category": "Lean 4",
 				"title": "Open Documentation View",
-				"description": "Open documentation found in local 'html' folder in a separate web view panel"
+				"description": "Open documentation found in local 'html' folder in a separate web view panel."
 			}
 		],
 		"languages": [

vscode-lean4/src/config.ts

@@ -195,6 +195,22 @@ export function getInfoViewDebounceTime(): number {
     return workspace.getConfiguration('lean4.infoview').get('debounceTime', 50);
 }
 
+export function getInfoViewShowExpectedType(): boolean {
+    return workspace.getConfiguration('lean4.infoview').get('showExpectedType', true);
+}
+
+export function getInfoViewShowGoalNames(): boolean {
+    return workspace.getConfiguration('lean4.infoview').get('showGoalNames', true);
+}
+
+export function getInfoViewEmphasizeFirstGoal(): boolean {
+    return workspace.getConfiguration('lean4.infoview').get('emphasizeFirstGoal', false);
+}
+
+export function getInfoViewReverseTacticState(): boolean {
+    return workspace.getConfiguration('lean4.infoview').get('reverseTacticState', false);
+}
+
 export function getElaborationDelay(): number {
     return workspace.getConfiguration('lean4').get('elaborationDelay', 200);
 }