feat: add (un)select context menu options (#451)

Implements context menu entries to (un)select subexpressions in the
tactic state, in particular to unselect all of them at once.

lean4-infoview-api/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview-api",
-    "version": "0.4.0",
+    "version": "0.5.0",
     "description": "Types and API for @leanprover/infoview.",
     "scripts": {
         "watch": "tsc --watch",

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/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview",
-    "version": "0.7.10",
+    "version": "0.8.0",
     "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.4.0",
+        "@leanprover/infoview-api": "~0.5.0",
         "@vscode/codicons": "^0.0.32",
         "@vscode-elements/react-elements": "^0.5.0",
         "es-module-lexer": "^1.5.4",

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,23 @@ 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
+    /** An object that should be spliced into `data-vscode-context`. */
+    dataVscodeContext: object
 }
 
 /**
  * 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 +135,42 @@ export function useSelectableLocation(settings: SelectableLocationSettings): Sel
         }
     }
 
+    const dataVscodeContext = {
+        // 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`.
+        selectableLocationId: '',
+        unselectableLocationId: '',
+    }
+    const id = React.useId()
+    if (settings.isSelectable && locs) {
+        if (locs.isSelected(settings.loc)) dataVscodeContext.unselectableLocationId = id
+        else dataVscodeContext.selectableLocationId = 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

@@ -121,6 +121,8 @@ function TypePopupContents({ info }: TypePopupContentsProps) {
     // so let's not add it until someone really wants it.
     return (
         <LocationsContext.Provider value={undefined}>
+            {/* NOTE: we don't have to unset locations in `data-vscode-context` here
+            because popup contents are not DOM children, only React children. */}
             <div className="tooltip-code-content">
                 {interactive.state === 'resolved' ? (
                     <>
@@ -255,8 +257,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 +290,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)
@@ -314,11 +320,21 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps<SubexprInfo>)
                     ;(e as any)._InteractiveCodeTagSeen = {}
                     if (!(e.target instanceof Node)) return
                     if (!e.currentTarget.contains(e.target)) return
-                    // Select the pretty-printed code.
+
+                    // Select the pretty-printed code (see issue #311).
                     const sel = window.getSelection()
                     if (!sel) return
-                    sel.removeAllRanges()
                     sel.selectAllChildren(e.currentTarget)
+
+                    // If a context menu action other than cut/copy is chosen,
+                    // the auto-selection we made above should be removed.
+                    // We hack this by tagging the first auto-selected range with a special property,
+                    // and removing any selection on which the identifier is present in a global handler.
+                    if (0 < sel.rangeCount) (sel.getRangeAt(0) as any)._InteractiveCodeTagAutoSelection = {}
+
+                    // Hide the tooltip when a context menu is opened
+                    // by simulating a click-outside.
+                    ht.onClickOutside()
                 }}
             >
                 {tt.tooltip}

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,13 @@ 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 comments on `InteractiveCodeTag`.
+            const sel = window.getSelection()
+            if (sel && 0 < sel.rangeCount && '_InteractiveCodeTagAutoSelection' in sel.getRangeAt(0))
+                sel.removeAllRanges()
+        },
         // See https://rollupjs.org/guide/en/#avoiding-eval
         // eslint-disable-next-line @typescript-eslint/no-implied-eval
         runTestScript: async script => new Function(script)(),