feat: selection via context menu

lean4-infoview-api/src/infoviewApi.ts

@@ -108,6 +108,18 @@ export type InfoviewActionKind =
 
 export type InfoviewAction = { kind: InfoviewActionKind }
 
+export type ContextMenuEntry = 'goToDefinition' | 'select' | 'unselect' | 'unselectAll'
+
+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 +159,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/src/infoview/editorConnection.ts

@@ -1,6 +1,7 @@
 import type { Location, ShowDocumentParams } from 'vscode-languageserver-protocol'
 
 import {
+    ContextMenuAction,
     EditorApi,
     InfoviewAction,
     InfoviewActionKind,
@@ -12,9 +13,14 @@ 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>
 }
 
 /** Provides higher-level wrappers around functionality provided by the editor,

lean4-infoview/src/infoview/goalLocation.tsx

@@ -5,6 +5,8 @@ Authors: E.W.Ayers, Wojciech Nawrocki
 */
 import { FVarId, MVarId, SubexprPos } from '@leanprover/infoview-api'
 import * as React from 'react'
+import { EditorContext } from './contexts'
+import { useEvent } from './util'
 
 /**
  * A location within a goal. It is either:
@@ -60,16 +62,19 @@ export namespace GoalsLocation {
 }
 
 /**
- * An interface available through a React context in components where selecting subexpressions
- * makes sense. Currently this is only the goal state display. There, {@link GoalLocation}s can be
- * selected. */
+ * An interface available through a React context in components
+ * where selecting subexpressions makes sense.
+ * Currently, subexpressions can only be selected in the tactic state.
+ * We use {@link GoalsLocation} to represent subexpression positions in a goal.
+ */
 export interface Locations {
     isSelected: (l: GoalsLocation) => boolean
     setSelected: (l: GoalsLocation, fn: React.SetStateAction<boolean>) => void
     /**
-     * A template for the location of the current component. It is defined if and only if the current
-     * component is a subexpression of a selectable expression. We use
-     * {@link GoalsLocation.withSubexprPos} to map this template to a complete location. */
+     * A template for the location of the current component.
+     * It is defined if and only if the current component is a subexpression of a selectable expression.
+     * We use {@link GoalsLocation.withSubexprPos} to map this template to a complete location.
+     */
     subexprTemplate?: GoalsLocation
 }
 
@@ -88,16 +93,22 @@ export interface SelectableLocation {
     /** Returns whether propagation of the click event within the same handler should be stopped. */
     onClick: (e: React.MouseEvent<HTMLSpanElement, MouseEvent>) => boolean
     onPointerDown: (e: React.PointerEvent<HTMLSpanElement>) => void
+    dataVscodeContext: any
 }
 
 /**
  * Logic for a component that can be selected using Shift-click and is highlighted when selected.
  *
- * The hook returns a string of CSS classes containing `highlight-selected` when appropriate,
- * as well as event handlers which the the caller must attach to the component.
+ * The hook returns
+ * - a string of CSS classes containing `highlight-selected` when appropriate; and
+ * - event handlers which the the caller must attach to the component; and
+ * - an object to append to `data-vscode-context`
+ *   in order to display context menu entries to (un)select this location in VSCode.
  */
 export function useSelectableLocation(settings: SelectableLocationSettings): SelectableLocation {
     const locs = React.useContext(LocationsContext)
+    const ec = React.useContext(EditorContext)
+
     let className: string = ''
     if (settings.isSelectable && locs && locs.isSelected(settings.loc)) {
         className += 'highlight-selected '
@@ -123,9 +134,42 @@ export function useSelectableLocation(settings: SelectableLocationSettings): Sel
         }
     }
 
+    const dataVscodeContext: any = {
+        // We set both IDs to an invalid value by default
+        // in order to clear ancestors' locations in this span
+        // (`data-vscode-context` fields are overridden by child components).
+        // The value can be anything that will not be returned from `useId`.
+        locationSelectId: '',
+        locationUnselectId: '',
+    }
+    const id = React.useId()
+    if (settings.isSelectable && locs) {
+        if (locs.isSelected(settings.loc)) dataVscodeContext.locationUnselectId = id
+        else dataVscodeContext.locationSelectId = id
+    }
+    useEvent(
+        ec.events.clickedContextMenu,
+        _ => {
+            if (!settings.isSelectable || !locs) return
+            locs.setSelected(settings.loc, true)
+        },
+        [locs, settings],
+        `select:${id}`,
+    )
+    useEvent(
+        ec.events.clickedContextMenu,
+        _ => {
+            if (!settings.isSelectable || !locs) return
+            locs.setSelected(settings.loc, false)
+        },
+        [locs, settings],
+        `unselect:${id}`,
+    )
+
     return {
         className,
         onClick,
         onPointerDown,
+        dataVscodeContext,
     }
 }

lean4-infoview/src/infoview/goals.tsx

@@ -113,6 +113,7 @@ function HypName({ name, isInserted, isRemoved, mvarId, fvarId }: HypNameProps)
             <span
                 ref={ref}
                 className={namecls}
+                data-vscode-context={JSON.stringify(sl.dataVscodeContext)}
                 onPointerOver={e => hhl.onPointerOver(e)}
                 onPointerOut={e => hhl.onPointerOut(e)}
                 onPointerMove={e => hhl.onPointerMove(e)}

lean4-infoview/src/infoview/info.tsx

@@ -147,10 +147,20 @@ interface GoalInfoDisplayProps {
 
 function GoalInfoDisplay(props: GoalInfoDisplayProps) {
     const { pos, goals, termGoal, userWidgets } = props
+    const ec = React.useContext(EditorContext)
 
     const config = React.useContext(ConfigContext)
 
     const [selectedLocs, setSelectedLocs] = React.useState<GoalsLocation[]>([])
+    const selectedLocationsId = React.useId()
+    useEvent(
+        ec.events.clickedContextMenu,
+        _ => {
+            setSelectedLocs([])
+        },
+        [setSelectedLocs],
+        `unselectAll:${selectedLocationsId}`,
+    )
 
     // https://react.dev/learn/you-might-not-need-an-effect#adjusting-some-state-when-a-prop-changes
     const [prevPos, setPrevPos] = React.useState<DocumentPosition>(pos)
@@ -180,7 +190,9 @@ function GoalInfoDisplay(props: GoalInfoDisplayProps) {
     return (
         <>
             <LocationsContext.Provider value={locs}>
-                <FilteredGoals key="goals" headerChildren="Tactic state" initiallyOpen goals={goals} displayCount />
+                <span data-vscode-context={JSON.stringify({ selectedLocationsId })}>
+                    <FilteredGoals key="goals" headerChildren="Tactic state" initiallyOpen goals={goals} displayCount />
+                </span>
             </LocationsContext.Provider>
             <FilteredGoals
                 key="term-goal"

lean4-infoview/src/infoview/interactiveCode.tsx

@@ -255,8 +255,12 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps<SubexprInfo>)
     // parameterized with `data-vscode-context`. We then use this context to execute the
     // command in the context of the correct interactive code tag in the InfoView.
     const interactiveCodeTagId = React.useId()
-    const vscodeContext = { interactiveCodeTagId }
-    useEvent(ec.events.goToDefinition, async _ => void execGoToLoc(true), [execGoToLoc], interactiveCodeTagId)
+    useEvent(
+        ec.events.clickedContextMenu,
+        async _ => void execGoToLoc(true),
+        [execGoToLoc],
+        `goToDefinition:${interactiveCodeTagId}`,
+    )
 
     const ht = useHoverTooltip(ref, <TypePopupContents info={ct} />, (e, cont) => {
         // On ctrl-click or ⌘-click, if location is known, go to it in the editor
@@ -284,7 +288,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps<SubexprInfo>)
             <span
                 ref={ref}
                 className={className}
-                data-vscode-context={JSON.stringify(vscodeContext)}
+                data-vscode-context={JSON.stringify({ ...sl.dataVscodeContext, interactiveCodeTagId })}
                 data-has-tooltip-on-hover
                 onClick={e => {
                     const stopClick = sl.onClick(e)

lean4-infoview/src/infoview/main.tsx

@@ -128,7 +128,7 @@ export function renderInfoview(editorApi: EditorApi, uiElement: HTMLElement): In
         changedInfoviewConfig: new EventEmitter(),
         runTestScript: new EventEmitter(),
         requestedAction: new EventEmitter(),
-        goToDefinition: new EventEmitter(),
+        clickedContextMenu: new EventEmitter(),
     }
 
     // Challenge: write a type-correct fn from `Eventify<T>` to `T` without using `any`
@@ -147,7 +147,8 @@ export function renderInfoview(editorApi: EditorApi, uiElement: HTMLElement): In
         changedCursorLocation: async loc => editorEvents.changedCursorLocation.fire(loc),
         changedInfoviewConfig: async conf => editorEvents.changedInfoviewConfig.fire(conf),
         requestedAction: async action => editorEvents.requestedAction.fire(action, action.kind),
-        goToDefinition: async id => editorEvents.goToDefinition.fire(id, id),
+        clickedContextMenu: async action =>
+            editorEvents.clickedContextMenu.fire(action, `${action.entry}:${action.id}`),
         // See https://rollupjs.org/guide/en/#avoiding-eval
         // eslint-disable-next-line @typescript-eslint/no-implied-eval
         runTestScript: async script => new Function(script)(),

vscode-lean4/package.json

@@ -271,6 +271,24 @@
                 "title": "Go to Definition",
                 "description": "This command is an implementation detail of the 'Go to Definition' context menu option in the infoview."
             },
+            {
+                "command": "lean4.infoview.select",
+                "category": "Lean 4",
+                "title": "Select",
+                "description": "This command is an implementation detail of the 'Select' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.unselect",
+                "category": "Lean 4",
+                "title": "Unselect",
+                "description": "This command is an implementation detail of the 'Unselect' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.unselectAll",
+                "category": "Lean 4",
+                "title": "Unselect All",
+                "description": "This command is an implementation detail of the 'Unselect All' context menu option in the infoview."
+            },
             {
                 "command": "lean4.loogle.search",
                 "category": "Lean 4",
@@ -876,6 +894,18 @@
                 {
                     "command": "lean4.infoview.goToDefinition",
                     "when": "webviewId == 'lean4_infoview' && interactiveCodeTagId"
+                },
+                {
+                    "command": "lean4.infoview.select",
+                    "when": "webviewId == 'lean4_infoview' && locationSelectId"
+                },
+                {
+                    "command": "lean4.infoview.unselect",
+                    "when": "webviewId == 'lean4_infoview' && locationUnselectId"
+                },
+                {
+                    "command": "lean4.infoview.unselectAll",
+                    "when": "webviewId == 'lean4_infoview' && selectedLocationsId"
                 }
             ]
         },

vscode-lean4/src/infoview.ts

@@ -365,7 +365,16 @@ export class InfoProvider implements Disposable {
                 this.webviewPanel?.api.requestedAction({ kind: 'togglePin' }),
             ),
             commands.registerCommand('lean4.infoview.goToDefinition', args =>
-                this.webviewPanel?.api.goToDefinition(args.interactiveCodeTagId),
+                this.webviewPanel?.api.clickedContextMenu({ entry: 'goToDefinition', id: args.interactiveCodeTagId }),
+            ),
+            commands.registerCommand('lean4.infoview.select', args =>
+                this.webviewPanel?.api.clickedContextMenu({ entry: 'select', id: args.locationSelectId }),
+            ),
+            commands.registerCommand('lean4.infoview.unselect', args =>
+                this.webviewPanel?.api.clickedContextMenu({ entry: 'unselect', id: args.locationUnselectId }),
+            ),
+            commands.registerCommand('lean4.infoview.unselectAll', args =>
+                this.webviewPanel?.api.clickedContextMenu({ entry: 'unselectAll', id: args.selectedLocationsId }),
             ),
         )
     }