From 12241daa36409142c1ba8022d1329d24df716ad1 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 29 May 2023 11:40:17 +0100 Subject: [PATCH 1/4] fix: contravariance --- lean4-infoview/src/infoview/collapsing.tsx | 7 +++---- lean4-infoview/src/infoview/messages.tsx | 2 +- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/lean4-infoview/src/infoview/collapsing.tsx b/lean4-infoview/src/infoview/collapsing.tsx index 61e0188b..bc46b1e1 100644 --- a/lean4-infoview/src/infoview/collapsing.tsx +++ b/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>>; + setOpenRef?: (_: React.Dispatch>) => void; } /** Like `
` 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
+ if (setOpenRef) setOpenRef(setOpen); + return
{summary} { isOpen && children }
; diff --git a/lean4-infoview/src/infoview/messages.tsx b/lean4-infoview/src/infoview/messages.tsx index 8991f991..428a85f7 100644 --- a/lean4-infoview/src/infoview/messages.tsx +++ b/lean4-infoview/src/infoview/messages.tsx @@ -129,7 +129,7 @@ export function AllMessages({uri: uri0}: { uri: DocumentUri }) { return ( -
+
setOpenRef.current = r} initiallyOpen={!config.autoOpenShowsGoal}> All Messages ({diags.length}) From a7a42523414426204fc61fe22fd1315fdb19fb5e Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 29 May 2023 12:09:59 +0100 Subject: [PATCH 2/4] feat: more config options for infoview Co-authored-by: Patrick Massot --- README.md | 10 +++++++ lean4-infoview-api/src/infoviewApi.ts | 17 ++++++++---- vscode-lean4/package.json | 38 +++++++++++++++++++++------ vscode-lean4/src/config.ts | 16 +++++++++++ vscode-lean4/src/infoview.ts | 12 ++++++++- 5 files changed, 79 insertions(+), 14 deletions(-) diff --git a/README.md b/README.md index f57942ac..6ef51844 100644 --- a/README.md +++ b/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 Ctrl+Alt+e `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 or 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 ctrl+alt+e 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. diff --git a/lean4-infoview-api/src/infoviewApi.ts b/lean4-infoview-api/src/infoviewApi.ts index 20c54e31..84d13416 100644 --- a/lean4-infoview-api/src/infoviewApi.ts +++ b/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 { diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index 84ef1404..587093c6 100644 --- a/vscode-lean4/package.json +++ b/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,11 +239,7 @@ "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", @@ -231,6 +247,12 @@ "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": [ diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts index 13d08416..58964545 100644 --- a/vscode-lean4/src/config.ts +++ b/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); } diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index 9b072fc7..223e0142 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -10,6 +10,10 @@ import { EditorApi, InfoviewApi, LeanFileProgressParams, TextInsertKind, import { LeanClient } from './leanclient'; import { getEditorLineHeight, getInfoViewAllErrorsOnLine, getInfoViewAutoOpen, getInfoViewAutoOpenShowsGoal, getInfoViewDebounceTime, + getInfoViewEmphasizeFirstGoal, + getInfoViewReverseTacticState, + getInfoViewShowExpectedType, + getInfoViewShowGoalNames, getInfoViewStyle, minIfProd, prodOrDev } from './config'; import { Rpc } from './rpc'; import { LeanClientProvider } from './utils/clientProvider' @@ -285,6 +289,8 @@ export class InfoProvider implements Disposable { () => this.webviewPanel?.api.requestedAction({kind: 'copyToComment'})), commands.registerCommand('lean4.infoView.toggleUpdating', () => this.webviewPanel?.api.requestedAction({kind: 'togglePaused'})), + commands.registerCommand('lean4.infoView.toggleExpectedType', () => + this.webviewPanel?.api.requestedAction({kind: 'toggleExpectedType'})), commands.registerTextEditorCommand('lean4.infoView.toggleStickyPosition', () => this.webviewPanel?.api.requestedAction({kind: 'togglePin'})), ); @@ -575,6 +581,10 @@ export class InfoProvider implements Disposable { allErrorsOnLine: getInfoViewAllErrorsOnLine(), autoOpenShowsGoal: getInfoViewAutoOpenShowsGoal(), debounceTime: getInfoViewDebounceTime(), + showExpectedType: getInfoViewShowExpectedType(), + showGoalNames: getInfoViewShowGoalNames(), + emphasizeFirstGoal: getInfoViewEmphasizeFirstGoal(), + reverseTacticState: getInfoViewReverseTacticState() }); } @@ -604,8 +614,8 @@ export class InfoProvider implements Disposable { private onLanguageChanged() { this.autoOpen().then(async () => { - await this.sendPosition(); await this.sendConfig(); + await this.sendPosition(); }).catch(() => {}); } From 79141e8f429b0f8fe6ffc569b70218f52771d5b9 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 29 May 2023 12:10:39 +0100 Subject: [PATCH 3/4] fix: send config earlier So that the infoview never renders without the user-specified settings. --- vscode-lean4/src/infoview.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index 223e0142..52827915 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -563,12 +563,12 @@ export class InfoProvider implements Disposable { // so that it has up-to-date information. if (client?.initializeResult) { logger.log('[InfoProvider] initInfoView!') + await this.sendConfig(); await this.webviewPanel?.api.serverStopped(undefined); // clear any server stopped state await this.webviewPanel?.api.serverRestarted(client.initializeResult); await this.sendDiagnostics(client); await this.sendProgress(client); await this.sendPosition(); - await this.sendConfig(); } else if (client == null) { logger.log('[InfoProvider] initInfoView got null client.') } else { From 7669a129c99fbc936c9bc191ae44d87b3bffb4e4 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 29 May 2023 12:12:51 +0100 Subject: [PATCH 4/4] feat: implement new options Co-authored-by: Patrick Massot --- lean4-infoview/src/infoview/goals.tsx | 72 +++++++++++++------ lean4-infoview/src/infoview/index.css | 5 ++ lean4-infoview/src/infoview/info.tsx | 17 ++++- lean4-infoview/src/infoview/traceExplorer.tsx | 5 +- 4 files changed, 73 insertions(+), 26 deletions(-) diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx index ed4be466..17cc8aea 100644 --- a/lean4-infoview/src/infoview/goals.tsx +++ b/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) => { - 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) => ), + !filter.reverse && goalLi + ] + + if (goal.userName && config.showGoalNames) { return
case {goal.userName} - {filter.reverse && goalLi} - {hyps.map((h, i) => )} - {!filter.reverse && goalLi} + {children}
} else return
- {filter.reverse && goalLi} - {hyps.map((h, i) => )} - {!filter.reverse && goalLi} + {children}
}) 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 No goals } else { + const config = React.useContext(ConfigContext) + const unemphasizeCn = 'o-70 font-size-code-smaller' return <> {displayCount && {nGoals} {1 < nGoals ? 'goals' : 'goal'}} - {goals.goals.map((g, i) => )} + {goals.goals.map((g, i) => + )} } } @@ -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 = const [goalFilters, setGoalFilters] = React.useState( - { 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 = + const setOpenRef = React.useRef>>() + useEvent(ec.events.requestedAction, act => { + if (act.kind === togglingAction && setOpenRef.current !== undefined) { + setOpenRef.current(t => !t) + } + }) + return
-
+
setOpenRef.current = r} initiallyOpen={initiallyOpen}> {headerChildren} {copyToCommentButton}{sortButton}{filterButton}
- {goals && } + {goals && }
-
+
}) diff --git a/lean4-infoview/src/infoview/index.css b/lean4-infoview/src/infoview/index.css index 0c6cb414..dcb9f474 100644 --- a/lean4-infoview/src/infoview/index.css +++ b/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); diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx index 735da6c5..cb23841e 100644 --- a/lean4-infoview/src/infoview/info.tsx +++ b/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) => { { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again. } - + - + {userWidgets.map(widget =>
{widget.name} diff --git a/lean4-infoview/src/infoview/traceExplorer.tsx b/lean4-infoview/src/infoview/traceExplorer.tsx index 6c69a9f1..d62c9940 100644 --- a/lean4-infoview/src/infoview/traceExplorer.tsx +++ b/lean4-infoview/src/infoview/traceExplorer.tsx @@ -113,7 +113,10 @@ function InteractiveMessageTag({tag: embed}: InteractiveTagProps): JSX if ('expr' in embed) return else if ('goal' in embed) - return + return else if ('lazyTrace' in embed) return else if ('trace' in embed)