Tracking PR for monaco

.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') }}

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.5",
     "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 => {