Sync

.github/workflows/on-push.yml

@@ -55,6 +55,18 @@ jobs:
         run: |
           npm publish --workspace=lean4-infoview --access=public
 
+      - name: Try publishing unicode-input
+        if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
+        continue-on-error: true
+        run: |
+          npm publish --workspace=lean4-unicode-input --access=public
+
+      - name: Try publishing unicode-input-component
+        if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
+        continue-on-error: true
+        run: |
+          npm publish --workspace=lean4-unicode-input-component --access=public
+
       - name: Package
         run: npm run package --workspace=lean4
         if: ${{ !startsWith(github.ref, 'refs/tags/v') || !endsWith(github.ref, '-pre') }}

.husky/pre-commit

@@ -1,4 +0,0 @@
-#!/bin/sh
-. "$(dirname "$0")/_/husky.sh"
-
-npx lint-staged

README.md

@@ -10,7 +10,7 @@ After installing this extension, a 'Welcome' page with a setup guide should open
 - Setting up a Lean 4 project
 - Troubleshooting issues
 
-If the setup guide does not open automatically, you can still open it manually by opening an empty file, clicking on the ∀-symbol in the top right and selecting 'Documentation…' > 'Docs: Show Setup Guide'.
+If the setup guide does not open automatically, you can still open it manually by opening an empty file, clicking on the ∀-symbol in the top right and selecting 'Documentation…' > 'Show Setup Guide'.
 
   ![Setup guide with instructions for how to re-open the setup guide manually](https://github.com/leanprover/vscode-lean4/raw/HEAD/vscode-lean4/images/setup_guide.png)
 

lean4-infoview-api/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview-api",
-    "version": "0.4.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,6 +120,46 @@ export type InfoviewActionKind =
 
 export type InfoviewAction = { kind: InfoviewActionKind }
 
+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
+    /**
+     * An entry-specific identifier extracted from `data-vscode-context`.
+     * For example, for `goToDefinition` it is the value of `interactiveCodeTagId`.
+     * See https://code.visualstudio.com/api/extension-guides/webview#context-menus.
+     */
+    id: string
+}
+
 /** Interface the hosting editor uses to talk to the InfoView WebView. */
 export interface InfoviewApi {
     /** Must be called exactly once on initialization with the current cursor position. */
@@ -147,11 +199,9 @@ export interface InfoviewApi {
     requestedAction(action: InfoviewAction): Promise<void>
 
     /**
-     * Must fire whenever the user requests to go to a definition using the infoview context menu.
-     * `interactiveCodeTagId` is obtainable from the `data-vscode-context` field in
-     * `InteractiveCodeTag`s in the InfoView. See https://code.visualstudio.com/api/extension-guides/webview#context-menus.
-     */
-    goToDefinition(interactiveCodeTagId: string): Promise<void>
+     * Must fire whenever the user clicks an infoview-specific context menu entry.
+     **/
+    clickedContextMenu(action: ContextMenuAction): Promise<void>
 
     /**
      * Execute the given JavaScript code inside the infoview. Must not be used

lean4-infoview-api/src/lspTypes.ts

@@ -1,16 +1,30 @@
 import type {
     Diagnostic,
     DocumentUri,
+    integer,
     Range,
     TextDocumentPositionParams,
     VersionedTextDocumentIdentifier,
 } from 'vscode-languageserver-protocol'
 
 // Lean 4 extensions to LSP.
 
+export enum LeanTag {
+    UnsolvedGoals = 1, // introduced in 2025-03-05
+    GoalsAccomplished = 2, // introduced in 2025-03-05
+}
+
 /** Used in place of {@link Diagnostic} within `textDocument/publishDiagnostics`. */
 export interface LeanDiagnostic extends Diagnostic {
     fullRange?: Range // introduced in 2021-03-10
+    isSilent?: boolean // introduced in 2025-03-05
+    leanTags?: LeanTag[] // introduced in 2025-03-05
+}
+
+export interface LeanPublishDiagnosticsParams {
+    uri: DocumentUri
+    version?: integer
+    diagnostics: LeanDiagnostic[]
 }
 
 export interface PlainGoal {

lean4-infoview/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview",
-    "version": "0.7.9",
+    "version": "0.8.5",
     "description": "An interactive display for the Lean 4 theorem prover.",
     "scripts": {
         "watch": "rollup --config --environment NODE_ENV:development --watch",
@@ -10,12 +10,12 @@
     },
     "exports": {
         ".": {
-            "default": "./dist/index.production.min.js",
-            "types": "./dist/index.d.ts"
+            "types": "./dist/index.d.ts",
+            "default": "./dist/index.production.min.js"
         },
         "./loader": {
-            "default": "./dist/loader.production.min.js",
-            "types": "./dist/loader.d.ts"
+            "types": "./dist/loader.d.ts",
+            "default": "./dist/loader.production.min.js"
         },
         "./package.json": "./package.json"
     },
@@ -42,16 +42,17 @@
         "react-dom": "^18.2.0",
         "react-markdown": "^9.0.1",
         "react-syntax-highlighter": "^15.5.0",
-        "remark-math": "^6.0.0",
         "rehype-mathjax": "^6.0.0",
+        "remark-math": "^6.0.0",
         "rollup": "^4.24.0",
         "rollup-plugin-css-only": "^4.3.0",
         "typescript": "^5.4.5"
     },
     "dependencies": {
-        "@leanprover/infoview-api": "~0.4.0",
-        "@vscode/codicons": "^0.0.32",
+        "@leanprover/infoview-api": "~0.7.0",
         "@vscode-elements/react-elements": "^0.5.0",
+        "@vscode/codicons": "^0.0.32",
+        "es-module-lexer": "^1.6.0",
         "es-module-shims": "^1.7.3",
         "react-fast-compare": "^3.2.2",
         "tachyons": "^4.12.0",

lean4-infoview/rollup.config.js

@@ -17,7 +17,11 @@ const output =
               compact: true,
               entryFileNames: '[name].production.min.js',
               chunkFileNames: '[name]-[hash].production.min.js',
-              plugins: [terser()],
+              plugins: [terser({
+                format: {
+                    comments: /webpackIgnore/,
+                }
+            })],
           }
         : {
               dir: 'dist',
@@ -74,7 +78,9 @@ const configs = [
     {
         output: {
             ...output,
-            // Put `es-module-shims` in shim mode with support for dynamic `import`
+            // Put `es-module-shims` in shim mode, needed to support dynamic `import`s.
+            // This code has to be set before `es-module-shims` is loaded,
+            // so we put it in the Rollup intro.
             intro: 'window.esmsInitOptions = { shimMode: true }',
         },
         plugins,

lean4-infoview/src/index.tsx

@@ -8,7 +8,7 @@ export { EditorContext, EnvPosContext, VersionContext } from './infoview/context
 export { EditorConnection } from './infoview/editorConnection'
 export { GoalLocation, GoalsLocation, LocationsContext } from './infoview/goalLocation'
 export { InteractiveCode, InteractiveCodeProps, Markdown } from './infoview/interactiveCode'
-export { renderInfoview } from './infoview/main'
+export { renderInfoview, InfoviewFc } from './infoview/main'
 export { RpcContext, useRpcSession } from './infoview/rpcSessions'
 export { ServerVersion } from './infoview/serverVersion'
 export { DynamicComponent, DynamicComponentProps, PanelWidgetProps, importWidgetModule } from './infoview/userWidget'

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 => {

lean4-infoview/src/infoview/contexts.ts

@@ -1,7 +1,12 @@
 import * as React from 'react'
-import type { Diagnostic, DocumentUri } from 'vscode-languageserver-protocol'
+import type { DocumentUri } from 'vscode-languageserver-protocol'
 
-import { defaultInfoviewConfig, InfoviewConfig, LeanFileProgressProcessingInfo } from '@leanprover/infoview-api'
+import {
+    defaultInfoviewConfig,
+    InfoviewConfig,
+    LeanDiagnostic,
+    LeanFileProgressProcessingInfo,
+} from '@leanprover/infoview-api'
 
 import { EditorConnection } from './editorConnection'
 import { ServerVersion } from './serverVersion'
@@ -13,7 +18,7 @@ export const EditorContext = React.createContext<EditorConnection>(null as any)
 export const VersionContext = React.createContext<ServerVersion | undefined>(undefined)
 
 export const ConfigContext = React.createContext<InfoviewConfig>(defaultInfoviewConfig)
-export const LspDiagnosticsContext = React.createContext<Map<DocumentUri, Diagnostic[]>>(new Map())
+export const LspDiagnosticsContext = React.createContext<Map<DocumentUri, LeanDiagnostic[]>>(new Map())
 export const ProgressContext = React.createContext<Map<DocumentUri, LeanFileProgressProcessingInfo[]>>(new Map())
 
 /**

lean4-infoview/src/infoview/editorConnection.ts

@@ -1,6 +1,7 @@
 import type { Location, ShowDocumentParams } from 'vscode-languageserver-protocol'
 
 import {
+    ContextMenuAction,
     EditorApi,
     InfoviewAction,
     InfoviewActionKind,
@@ -12,9 +13,15 @@ import {
 import { EventEmitter, Eventify } from './event'
 import { DocumentPosition } from './util'
 
-export type EditorEvents = Omit<Eventify<InfoviewApi>, 'requestedAction' | 'goToDefinition'> & {
+export type EditorEvents = Omit<Eventify<InfoviewApi>, 'requestedAction' | 'clickedContextMenu'> & {
     requestedAction: EventEmitter<InfoviewAction, InfoviewActionKind>
-    goToDefinition: EventEmitter<string, string>
+    /**
+     * Must fire whenever the user clicks an infoview-specific context menu entry.
+     *
+     * Keys for this event are of the form `` `${action.entry}:${action.id}` ``.
+     */
+    clickedContextMenu: EventEmitter<ContextMenuAction, string>
+    goToDefinition?: EventEmitter<number, number>
 }
 
 /** Provides higher-level wrappers around functionality provided by the editor,