From 7f7c230b4d8e9a713d635814f8a4a0ec5925f5d6 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Mon, 1 Jul 2024 14:44:28 +0200 Subject: [PATCH 01/26] refactor: simplify subexpr loop control flow --- lean4-infoview/src/infoview/tooltips.tsx | 63 ++++++++++-------------- lean4-infoview/src/infoview/util.ts | 38 -------------- 2 files changed, 26 insertions(+), 75 deletions(-) diff --git a/lean4-infoview/src/infoview/tooltips.tsx b/lean4-infoview/src/infoview/tooltips.tsx index 0c9472169..c88c00b00 100644 --- a/lean4-infoview/src/infoview/tooltips.tsx +++ b/lean4-infoview/src/infoview/tooltips.tsx @@ -4,13 +4,7 @@ import * as ReactDOM from 'react-dom' import { arrow, autoPlacement, autoUpdate, FloatingArrow, offset, shift, size, useFloating } from '@floating-ui/react' import { ConfigContext } from './contexts' -import { - forwardAndUseRef, - forwardAndUseStateRef, - LogicalDomContext, - useLogicalDomObserver, - useOnClickOutside, -} from './util' +import { LogicalDomContext, useLogicalDomObserver, useOnClickOutside } from './util' export type TooltipProps = React.PropsWithChildren> & { reference: HTMLElement | null } @@ -70,15 +64,15 @@ export function Tooltip(props_: TooltipProps) { return ReactDOM.createPortal(floating, document.body) } -export const WithToggleableTooltip = forwardAndUseStateRef< - HTMLSpanElement, - React.HTMLProps & { - isTooltipShown: boolean - hideTooltip: () => void - tooltipChildren: React.ReactNode - } ->((props_, ref, setRef) => { +export type WithToggleableTooltipProps = React.HTMLProps & { + isTooltipShown: boolean + hideTooltip: () => void + tooltipChildren: React.ReactNode +} + +export function WithToggleableTooltip(props_: WithToggleableTooltipProps) { const { isTooltipShown, hideTooltip, tooltipChildren, ...props } = props_ + const [ref, setRef] = React.useState(null) // Since we do not want to hide the tooltip if the user is trying to select text in it, // we need both the "click outside" and "click inside" handlers here because they @@ -110,7 +104,7 @@ export const WithToggleableTooltip = forwardAndUseStateRef< ) -}) +} /** Hover state of an element. The pointer can be * - elsewhere (`off`) @@ -119,17 +113,17 @@ export const WithToggleableTooltip = forwardAndUseStateRef< */ export type HoverState = 'off' | 'over' | 'ctrlOver' +export type DetectHoverSpanProps = React.DetailedHTMLProps, HTMLSpanElement> & { + setHoverState: React.Dispatch> +} + /** An element which calls `setHoverState` when the hover state of its DOM children changes. * * It is implemented with JS rather than CSS in order to allow nesting of these elements. When nested, * only the smallest (deepest in the DOM tree) {@link DetectHoverSpan} has an enabled hover state. */ -export const DetectHoverSpan = forwardAndUseRef< - HTMLSpanElement, - React.DetailedHTMLProps, HTMLSpanElement> & { - setHoverState: React.Dispatch> - } ->((props_, ref, setRef) => { +export function DetectHoverSpan(props_: DetectHoverSpanProps) { const { setHoverState, ...props } = props_ + const ref = React.useRef(null) const onPointerEvent = (b: boolean, e: React.PointerEvent) => { // It's more composable to let pointer events bubble up rather than to call `stopPropagation`, @@ -168,7 +162,7 @@ export const DetectHoverSpan = forwardAndUseRef< return ( { onPointerEvent(true, e) if (props.onPointerOver) props.onPointerOver(e) @@ -186,7 +180,7 @@ export const DetectHoverSpan = forwardAndUseRef< {props.children} ) -}) +} /** Pinning a child tooltip has to also pin all ancestors. This context supports that. */ interface TipChainContext { @@ -195,19 +189,14 @@ interface TipChainContext { const TipChainContext = React.createContext({ pinParent: () => {} }) -/** Shows a tooltip when the children are hovered over or clicked. - * - * An `onClick` middleware can optionally be given in order to control what happens when the - * hoverable area is clicked. The middleware can invoke `next` to execute the default action - * which is to pin the tooltip open. */ -export const WithTooltipOnHover = forwardAndUseStateRef< - HTMLSpanElement, - Omit, 'onClick'> & { - tooltipChildren: React.ReactNode - onClick?: (event: React.MouseEvent, next: React.MouseEventHandler) => void - } ->((props_, ref, setRef) => { +export type WithTooltipOnHoverProps = Omit, 'onClick'> & { + tooltipChildren: React.ReactNode + onClick?: (event: React.MouseEvent, next: React.MouseEventHandler) => void +} + +export function WithTooltipOnHover(props_: WithTooltipOnHoverProps) { const { tooltipChildren, onClick: onClickProp, ...props } = props_ + const [ref, setRef] = React.useState(null) const config = React.useContext(ConfigContext) @@ -336,4 +325,4 @@ export const WithTooltipOnHover = forwardAndUseStateRef< ) -}) +} diff --git a/lean4-infoview/src/infoview/util.ts b/lean4-infoview/src/infoview/util.ts index e4e90f898..0028d71a6 100644 --- a/lean4-infoview/src/infoview/util.ts +++ b/lean4-infoview/src/infoview/util.ts @@ -216,44 +216,6 @@ export function addUniqueKeys(elems: T[], getId: (el: T) => string): Keyed }) } -/** Like `React.forwardRef`, but also allows reading the ref inside the forwarding component. - * Adapted from https://itnext.io/reusing-the-ref-from-forwardref-with-react-hooks-4ce9df693dd */ -export function forwardAndUseRef( - render: (props: P, ref: React.RefObject, setRef: (_: T | null) => void) => React.ReactElement | null, -): React.ForwardRefExoticComponent & React.RefAttributes> { - return React.forwardRef((props, ref) => { - const thisRef = React.useRef(null) - return render(props, thisRef, v => { - thisRef.current = v - if (!ref) return - if (typeof ref === 'function') { - ref(v) - } else { - ref.current = v - } - }) - }) -} - -/** Like `forwardAndUseRef`, but the ref is stored in state so that setting it triggers a render. - * Should only be used if re-rendering is necessary. */ -export function forwardAndUseStateRef( - render: (props: P, ref: T | null, setRef: (_: T | null) => void) => React.ReactElement | null, -): React.ForwardRefExoticComponent & React.RefAttributes> { - return React.forwardRef((props, ref) => { - const [thisRef, setThisRef] = React.useState(null) - return render(props, thisRef, v => { - setThisRef(v) - if (!ref) return - if (typeof ref === 'function') { - ref(v) - } else { - ref.current = v - } - }) - }) -} - export interface LogicalDomElement { contains(el: Node): boolean } From 374cbe12da069bffc91deb33b18a800e32cbce40 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 2 Jul 2024 16:18:21 +0200 Subject: [PATCH 02/26] refactor: start inlining --- lean4-infoview/src/infoview/index.css | 6 -- .../src/infoview/interactiveCode.tsx | 92 +++++++++++++++++-- vscode-lean4/src/infoview.ts | 1 + 3 files changed, 84 insertions(+), 15 deletions(-) diff --git a/lean4-infoview/src/infoview/index.css b/lean4-infoview/src/infoview/index.css index c26a5496d..ec8f3512b 100644 --- a/lean4-infoview/src/infoview/index.css +++ b/lean4-infoview/src/infoview/index.css @@ -49,12 +49,6 @@ body { font-weight: normal; } -/* Used to denote text highlighted by the pretty-print expression widget. */ -.highlightable { - border-radius: 2pt; - transition: background-color 100ms ease-in-out; -} - .highlight { background-color: var(--vscode-editor-selectionBackground) !important; } diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index b7b5c8169..73422987a 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -12,7 +12,7 @@ import { import { marked } from 'marked' import { Location } from 'vscode-languageserver-protocol' import { EditorContext } from './contexts' -import { GoalsLocation, LocationsContext, SelectableLocation } from './goalLocation' +import { GoalsLocation, LocationsContext } from './goalLocation' import { useRpcSession } from './rpcSessions' import { HoverState, WithToggleableTooltip, WithTooltipOnHover } from './tooltips' import { mapRpcError, useAsync, useEvent } from './util' @@ -192,6 +192,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) locs && locs.subexprTemplate && ct.subexprPos ? GoalsLocation.withSubexprPos(locs.subexprTemplate, ct.subexprPos) : undefined + const isSelected = locs && ourLoc && locs.isSelected(ourLoc) let spanClassName: string = hoverState === 'ctrlOver' && goToLoc !== undefined ? 'underline ' : '' if (ct.diffStatus) { @@ -206,6 +207,59 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) const vscodeContext = { interactiveCodeTagId } useEvent(ec.events.goToDefinition, async _ => void execGoToLoc(true), [execGoToLoc], interactiveCodeTagId) + ////////////////////////////////////////////////////////////////////////////////////////////////////////// + /* SelectableLocation */ + const [slHoverState, setSLHoverState] = React.useState('off') + let slSpanClassName: string = '' + if (slHoverState !== 'off') { + slSpanClassName += 'highlight ' + } else if (isSelected) { + slSpanClassName += 'highlight-selected ' + } + slSpanClassName += spanClassName + + const slSetHoverStateAll: React.Dispatch> = React.useCallback(val => { + setSLHoverState(val) + }, []) + + ////////////////////////////////////////////////////////////////////////////////////////////////////////// + /* DetectHoverSpan */ + const dhRef = React.useRef(null) + + const dhOnPointerEvent = (b: boolean, e: React.PointerEvent) => { + // It's more composable to let pointer events bubble up rather than to call `stopPropagation`, + // but we only want to handle hovers in the innermost component. So we record that the + // event was handled with a property. + // The `contains` check ensures that the node hovered over is a child in the DOM + // tree and not just a logical React child (see useLogicalDom and + // https://reactjs.org/docs/portals.html#event-bubbling-through-portals). + if (dhRef.current && e.target instanceof Node && dhRef.current.contains(e.target)) { + if ('_DetectHoverSpanSeen' in e) return + ;(e as any)._DetectHoverSpanSeen = {} + if (!b) slSetHoverStateAll('off') + else if (e.ctrlKey || e.metaKey) slSetHoverStateAll('ctrlOver') + else slSetHoverStateAll('over') + } + } + + React.useEffect(() => { + const onKeyDown = (e: KeyboardEvent) => { + if (e.key === 'Control' || e.key === 'Meta') slSetHoverStateAll(st => (st === 'over' ? 'ctrlOver' : st)) + } + + const onKeyUp = (e: KeyboardEvent) => { + if (e.key === 'Control' || e.key === 'Meta') slSetHoverStateAll(st => (st === 'ctrlOver' ? 'over' : st)) + } + + // Note: In VSCode these events do not fire when the webview is not in focus. + document.addEventListener('keydown', onKeyDown) + document.addEventListener('keyup', onKeyUp) + return () => { + document.removeEventListener('keydown', onKeyDown) + document.removeEventListener('keyup', onKeyUp) + } + }, [slSetHoverStateAll]) + return ( ) sel.selectAllChildren(e.currentTarget) }} > - { + // On shift-click, if we are in a context where selecting subexpressions makes sense, + // (un)select the current subexpression. + if (e.shiftKey && locs && ourLoc) { + locs.setSelected(ourLoc, on => !on) + e.stopPropagation() + } + }} + onPointerDown={e => { + // Since shift-click on this component is a custom selection, when shift is held prevent + // the default action which on text is to start a text selection. + if (e.shiftKey) e.preventDefault() + }} + onPointerOver={e => { + dhOnPointerEvent(true, e) + }} + onPointerOut={e => { + dhOnPointerEvent(false, e) + }} + onPointerMove={e => { + if (e.ctrlKey || e.metaKey) slSetHoverStateAll(st => (st === 'over' ? 'ctrlOver' : st)) + else slSetHoverStateAll(st => (st === 'ctrlOver' ? 'over' : st)) + }} > - - + + ) diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index 80dd41862..6f4986ccf 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -881,6 +881,7 @@ export class InfoProvider implements Disposable { Infoview +
From 910b351bc5dd46df447858281bef94ab883ad5a9 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 2 Jul 2024 16:56:33 +0200 Subject: [PATCH 03/26] refactor: more inlining --- .../src/infoview/interactiveCode.tsx | 215 ++++++++++++++---- lean4-infoview/src/infoview/tooltips.tsx | 4 +- 2 files changed, 170 insertions(+), 49 deletions(-) diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index 73422987a..d7caf42ca 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -11,11 +11,11 @@ import { } from '@leanprover/infoview-api' import { marked } from 'marked' import { Location } from 'vscode-languageserver-protocol' -import { EditorContext } from './contexts' +import { ConfigContext, EditorContext } from './contexts' import { GoalsLocation, LocationsContext } from './goalLocation' import { useRpcSession } from './rpcSessions' -import { HoverState, WithToggleableTooltip, WithTooltipOnHover } from './tooltips' -import { mapRpcError, useAsync, useEvent } from './util' +import { HoverState, TipChainContext, Tooltip, WithToggleableTooltip } from './tooltips' +import { LogicalDomContext, mapRpcError, useAsync, useEvent, useLogicalDomObserver, useOnClickOutside } from './util' export interface InteractiveTextComponentProps { fmt: TaggedText @@ -260,67 +260,188 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) } }, [slSetHoverStateAll]) + ////////////////////////////////////////////////////////////////////////////////////////////////////////// + /* WithTooltipOnHover */ + const [htRef, setHTRef] = React.useState(null) + + const htConfig = React.useContext(ConfigContext) + + // We are pinned when clicked, shown when hovered over, and otherwise hidden. + type TooltipState = 'pin' | 'show' | 'hide' + const [htState, setHTState] = React.useState('hide') + const htShouldShow = htState !== 'hide' + + const htTipChainCtx = React.useContext(TipChainContext) + React.useEffect(() => { + if (htState === 'pin') htTipChainCtx.pinParent() + }, [htState, htTipChainCtx]) + const newHTTipChainCtx = React.useMemo( + () => ({ + pinParent: () => { + setHTState('pin') + htTipChainCtx.pinParent() + }, + }), + [htTipChainCtx], + ) + + // Note: because tooltips are attached to `document.body`, they are not descendants of the + // hoverable area in the DOM tree. Thus the `contains` check fails for elements within tooltip + // contents and succeeds for elements within the hoverable. We can use this to distinguish them. + const htIsWithinHoverable = (el: EventTarget) => htRef && el instanceof Node && htRef.contains(el) + const [htLogicalSpanElt, htLogicalDomStorage] = useLogicalDomObserver({ current: htRef }) + + // We use timeouts for debouncing hover events. + const htTimeout = React.useRef() + const htClearTimeout = () => { + if (htTimeout.current) { + window.clearTimeout(htTimeout.current) + htTimeout.current = undefined + } + } + const htShowDelay = 500 + const htHideDelay = 300 + + const htIsModifierHeld = (e: React.MouseEvent) => e.altKey || e.ctrlKey || e.shiftKey || e.metaKey + + const htOnClick = (e: React.MouseEvent) => { + htClearTimeout() + setHTState(state => (state === 'pin' ? 'hide' : 'pin')) + e.stopPropagation() + } + + const htOnClickOutside = React.useCallback(() => { + htClearTimeout() + setHTState('hide') + }, []) + useOnClickOutside(htLogicalSpanElt, htOnClickOutside) + + const htIsPointerOverTooltip = React.useRef(false) + const htStartShowTimeout = () => { + htClearTimeout() + if (!htConfig.showTooltipOnHover) return + htTimeout.current = window.setTimeout(() => { + setHTState(state => (state === 'hide' ? 'show' : state)) + htTimeout.current = undefined + }, htShowDelay) + } + const htStartHideTimeout = () => { + htClearTimeout() + htTimeout.current = window.setTimeout(() => { + if (!htIsPointerOverTooltip.current) setHTState(state => (state === 'show' ? 'hide' : state)) + htTimeout.current = undefined + }, htHideDelay) + } + + const htOnPointerEnter = (e: React.PointerEvent) => { + htIsPointerOverTooltip.current = true + htClearTimeout() + } + + const htOnPointerLeave = (e: React.PointerEvent) => { + htIsPointerOverTooltip.current = false + htStartHideTimeout() + } + + function htGuardMouseEvent( + act: (_: React.MouseEvent) => void, + e: React.MouseEvent, + ) { + if ('_WithTooltipOnHoverSeen' in e) return + if (!htIsWithinHoverable(e.target)) return + ;(e as any)._WithTooltipOnHoverSeen = {} + act(e) + } + return ( setGoToDefErrorState(false)} > - } - onClick={(e, next) => { - // On ctrl-click or ⌘-click, if location is known, go to it in the editor - if (e.ctrlKey || e.metaKey) { - setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) - void execGoToLoc(false) - } else if (!e.shiftKey) next(e) - }} - onContextMenu={e => { - // Mark the event as seen so that parent handlers skip it. - // We cannot use `stopPropagation` as that prevents the VSC context menu from showing up. - if ('_InteractiveCodeTagSeen' in e) return - ;(e as any)._InteractiveCodeTagSeen = {} - if (!(e.target instanceof Node)) return - if (!e.currentTarget.contains(e.target)) return - // Select the pretty-printed code. - const sel = window.getSelection() - if (!sel) return - sel.removeAllRanges() - sel.selectAllChildren(e.currentTarget) - }} - > + { - // On shift-click, if we are in a context where selecting subexpressions makes sense, - // (un)select the current subexpression. - if (e.shiftKey && locs && ourLoc) { - locs.setSelected(ourLoc, on => !on) - e.stopPropagation() - } + htGuardMouseEvent(e => { + // On ctrl-click or ⌘-click, if location is known, go to it in the editor + if (e.ctrlKey || e.metaKey) { + setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) + void execGoToLoc(false) + } else if (!e.shiftKey) htOnClick(e) + }, e) + }} + onContextMenu={e => { + // Mark the event as seen so that parent handlers skip it. + // We cannot use `stopPropagation` as that prevents the VSC context menu from showing up. + if ('_InteractiveCodeTagSeen' in e) return + ;(e as any)._InteractiveCodeTagSeen = {} + if (!(e.target instanceof Node)) return + if (!e.currentTarget.contains(e.target)) return + // Select the pretty-printed code. + const sel = window.getSelection() + if (!sel) return + sel.removeAllRanges() + sel.selectAllChildren(e.currentTarget) }} onPointerDown={e => { - // Since shift-click on this component is a custom selection, when shift is held prevent - // the default action which on text is to start a text selection. - if (e.shiftKey) e.preventDefault() + // We have special handling for some modifier+click events, so prevent default browser + // events from interfering when a modifier is held. + if (htIsModifierHeld(e)) e.preventDefault() }} onPointerOver={e => { - dhOnPointerEvent(true, e) + if (!htIsModifierHeld(e)) { + htGuardMouseEvent(_ => htStartShowTimeout(), e) + } }} onPointerOut={e => { - dhOnPointerEvent(false, e) - }} - onPointerMove={e => { - if (e.ctrlKey || e.metaKey) slSetHoverStateAll(st => (st === 'over' ? 'ctrlOver' : st)) - else slSetHoverStateAll(st => (st === 'ctrlOver' ? 'over' : st)) + htGuardMouseEvent(_ => htStartHideTimeout(), e) }} > - + {htShouldShow && ( + + + + + + )} + { + // On shift-click, if we are in a context where selecting subexpressions makes sense, + // (un)select the current subexpression. + if (e.shiftKey && locs && ourLoc) { + locs.setSelected(ourLoc, on => !on) + e.stopPropagation() + } + }} + onPointerDown={e => { + // Since shift-click on this component is a custom selection, when shift is held prevent + // the default action which on text is to start a text selection. + if (e.shiftKey) e.preventDefault() + }} + onPointerOver={e => { + dhOnPointerEvent(true, e) + }} + onPointerOut={e => { + dhOnPointerEvent(false, e) + }} + onPointerMove={e => { + if (e.ctrlKey || e.metaKey) slSetHoverStateAll(st => (st === 'over' ? 'ctrlOver' : st)) + else slSetHoverStateAll(st => (st === 'ctrlOver' ? 'over' : st)) + }} + > + + - + ) } diff --git a/lean4-infoview/src/infoview/tooltips.tsx b/lean4-infoview/src/infoview/tooltips.tsx index c88c00b00..ce6f7523c 100644 --- a/lean4-infoview/src/infoview/tooltips.tsx +++ b/lean4-infoview/src/infoview/tooltips.tsx @@ -183,11 +183,11 @@ export function DetectHoverSpan(props_: DetectHoverSpanProps) { } /** Pinning a child tooltip has to also pin all ancestors. This context supports that. */ -interface TipChainContext { +export interface TipChainContext { pinParent(): void } -const TipChainContext = React.createContext({ pinParent: () => {} }) +export const TipChainContext = React.createContext({ pinParent: () => {} }) export type WithTooltipOnHoverProps = Omit, 'onClick'> & { tooltipChildren: React.ReactNode From 6b7dc8a6ffa3b9341a80b062033221915f931bc1 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 2 Jul 2024 17:40:22 +0200 Subject: [PATCH 04/26] refactor: more inlining --- .../src/infoview/interactiveCode.tsx | 76 ++++++++----------- 1 file changed, 30 insertions(+), 46 deletions(-) diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index d7caf42ca..28793bcc1 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -224,7 +224,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) ////////////////////////////////////////////////////////////////////////////////////////////////////////// /* DetectHoverSpan */ - const dhRef = React.useRef(null) + const [htRef, setHTRef] = React.useState(null) const dhOnPointerEvent = (b: boolean, e: React.PointerEvent) => { // It's more composable to let pointer events bubble up rather than to call `stopPropagation`, @@ -233,7 +233,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) // The `contains` check ensures that the node hovered over is a child in the DOM // tree and not just a logical React child (see useLogicalDom and // https://reactjs.org/docs/portals.html#event-bubbling-through-portals). - if (dhRef.current && e.target instanceof Node && dhRef.current.contains(e.target)) { + if (htRef && e.target instanceof Node && htRef.contains(e.target)) { if ('_DetectHoverSpanSeen' in e) return ;(e as any)._DetectHoverSpanSeen = {} if (!b) slSetHoverStateAll('off') @@ -262,8 +262,6 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) ////////////////////////////////////////////////////////////////////////////////////////////////////////// /* WithTooltipOnHover */ - const [htRef, setHTRef] = React.useState(null) - const htConfig = React.useContext(ConfigContext) // We are pinned when clicked, shown when hovered over, and otherwise hidden. @@ -362,9 +360,17 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) { + // On shift-click, if we are in a context where selecting subexpressions makes sense, + // (un)select the current subexpression. + if (e.shiftKey && locs && ourLoc) { + locs.setSelected(ourLoc, on => !on) + e.stopPropagation() + return + } htGuardMouseEvent(e => { // On ctrl-click or ⌘-click, if location is known, go to it in the editor if (e.ctrlKey || e.metaKey) { @@ -373,32 +379,38 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) } else if (!e.shiftKey) htOnClick(e) }, e) }} - onContextMenu={e => { - // Mark the event as seen so that parent handlers skip it. - // We cannot use `stopPropagation` as that prevents the VSC context menu from showing up. - if ('_InteractiveCodeTagSeen' in e) return - ;(e as any)._InteractiveCodeTagSeen = {} - if (!(e.target instanceof Node)) return - if (!e.currentTarget.contains(e.target)) return - // Select the pretty-printed code. - const sel = window.getSelection() - if (!sel) return - sel.removeAllRanges() - sel.selectAllChildren(e.currentTarget) - }} onPointerDown={e => { // We have special handling for some modifier+click events, so prevent default browser // events from interfering when a modifier is held. if (htIsModifierHeld(e)) e.preventDefault() }} onPointerOver={e => { + dhOnPointerEvent(true, e) if (!htIsModifierHeld(e)) { htGuardMouseEvent(_ => htStartShowTimeout(), e) } }} onPointerOut={e => { + dhOnPointerEvent(false, e) htGuardMouseEvent(_ => htStartHideTimeout(), e) }} + onPointerMove={e => { + if (e.ctrlKey || e.metaKey) slSetHoverStateAll(st => (st === 'over' ? 'ctrlOver' : st)) + else slSetHoverStateAll(st => (st === 'ctrlOver' ? 'over' : st)) + }} + onContextMenu={e => { + // Mark the event as seen so that parent handlers skip it. + // We cannot use `stopPropagation` as that prevents the VSC context menu from showing up. + if ('_InteractiveCodeTagSeen' in e) return + ;(e as any)._InteractiveCodeTagSeen = {} + if (!(e.target instanceof Node)) return + if (!e.currentTarget.contains(e.target)) return + // Select the pretty-printed code. + const sel = window.getSelection() + if (!sel) return + sel.removeAllRanges() + sel.selectAllChildren(e.currentTarget) + }} > {htShouldShow && ( @@ -411,35 +423,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) )} - { - // On shift-click, if we are in a context where selecting subexpressions makes sense, - // (un)select the current subexpression. - if (e.shiftKey && locs && ourLoc) { - locs.setSelected(ourLoc, on => !on) - e.stopPropagation() - } - }} - onPointerDown={e => { - // Since shift-click on this component is a custom selection, when shift is held prevent - // the default action which on text is to start a text selection. - if (e.shiftKey) e.preventDefault() - }} - onPointerOver={e => { - dhOnPointerEvent(true, e) - }} - onPointerOut={e => { - dhOnPointerEvent(false, e) - }} - onPointerMove={e => { - if (e.ctrlKey || e.metaKey) slSetHoverStateAll(st => (st === 'over' ? 'ctrlOver' : st)) - else slSetHoverStateAll(st => (st === 'ctrlOver' ? 'over' : st)) - }} - > - - + From 5b58639bac38a88c860df25b1bcfcfb1cd8bb348 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 2 Jul 2024 18:09:42 +0200 Subject: [PATCH 05/26] refactor: more inlining --- .../src/infoview/interactiveCode.tsx | 147 +++++++++--------- 1 file changed, 71 insertions(+), 76 deletions(-) diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index 28793bcc1..5c741d514 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -14,7 +14,7 @@ import { Location } from 'vscode-languageserver-protocol' import { ConfigContext, EditorContext } from './contexts' import { GoalsLocation, LocationsContext } from './goalLocation' import { useRpcSession } from './rpcSessions' -import { HoverState, TipChainContext, Tooltip, WithToggleableTooltip } from './tooltips' +import { HoverState, TipChainContext, Tooltip } from './tooltips' import { LogicalDomContext, mapRpcError, useAsync, useEvent, useLogicalDomObserver, useOnClickOutside } from './util' export interface InteractiveTextComponentProps { @@ -311,6 +311,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) const htOnClickOutside = React.useCallback(() => { htClearTimeout() setHTState('hide') + setGoToDefErrorState(false) }, []) useOnClickOutside(htLogicalSpanElt, htOnClickOutside) @@ -352,81 +353,75 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) } return ( - setGoToDefErrorState(false)} - > - - { - // On shift-click, if we are in a context where selecting subexpressions makes sense, - // (un)select the current subexpression. - if (e.shiftKey && locs && ourLoc) { - locs.setSelected(ourLoc, on => !on) - e.stopPropagation() - return - } - htGuardMouseEvent(e => { - // On ctrl-click or ⌘-click, if location is known, go to it in the editor - if (e.ctrlKey || e.metaKey) { - setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) - void execGoToLoc(false) - } else if (!e.shiftKey) htOnClick(e) - }, e) - }} - onPointerDown={e => { - // We have special handling for some modifier+click events, so prevent default browser - // events from interfering when a modifier is held. - if (htIsModifierHeld(e)) e.preventDefault() - }} - onPointerOver={e => { - dhOnPointerEvent(true, e) - if (!htIsModifierHeld(e)) { - htGuardMouseEvent(_ => htStartShowTimeout(), e) - } - }} - onPointerOut={e => { - dhOnPointerEvent(false, e) - htGuardMouseEvent(_ => htStartHideTimeout(), e) - }} - onPointerMove={e => { - if (e.ctrlKey || e.metaKey) slSetHoverStateAll(st => (st === 'over' ? 'ctrlOver' : st)) - else slSetHoverStateAll(st => (st === 'ctrlOver' ? 'over' : st)) - }} - onContextMenu={e => { - // Mark the event as seen so that parent handlers skip it. - // We cannot use `stopPropagation` as that prevents the VSC context menu from showing up. - if ('_InteractiveCodeTagSeen' in e) return - ;(e as any)._InteractiveCodeTagSeen = {} - if (!(e.target instanceof Node)) return - if (!e.currentTarget.contains(e.target)) return - // Select the pretty-printed code. - const sel = window.getSelection() - if (!sel) return - sel.removeAllRanges() - sel.selectAllChildren(e.currentTarget) - }} - > - {htShouldShow && ( - - - - - - )} - - - - + + { + // On shift-click, if we are in a context where selecting subexpressions makes sense, + // (un)select the current subexpression. + if (e.shiftKey && locs && ourLoc) { + locs.setSelected(ourLoc, on => !on) + e.stopPropagation() + return + } + htGuardMouseEvent(e => { + // On ctrl-click or ⌘-click, if location is known, go to it in the editor + if (e.ctrlKey || e.metaKey) { + setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) + void execGoToLoc(false) + } else if (!e.shiftKey) htOnClick(e) + }, e) + if (!window.getSelection()?.toString()) setGoToDefErrorState(false) + }} + onPointerDown={e => { + // We have special handling for some modifier+click events, so prevent default browser + // events from interfering when a modifier is held. + if (htIsModifierHeld(e)) e.preventDefault() + }} + onPointerOver={e => { + dhOnPointerEvent(true, e) + if (!htIsModifierHeld(e)) { + htGuardMouseEvent(_ => htStartShowTimeout(), e) + } + }} + onPointerOut={e => { + dhOnPointerEvent(false, e) + htGuardMouseEvent(_ => htStartHideTimeout(), e) + }} + onPointerMove={e => { + if (e.ctrlKey || e.metaKey) slSetHoverStateAll(st => (st === 'over' ? 'ctrlOver' : st)) + else slSetHoverStateAll(st => (st === 'ctrlOver' ? 'over' : st)) + }} + onContextMenu={e => { + // Mark the event as seen so that parent handlers skip it. + // We cannot use `stopPropagation` as that prevents the VSC context menu from showing up. + if ('_InteractiveCodeTagSeen' in e) return + ;(e as any)._InteractiveCodeTagSeen = {} + if (!(e.target instanceof Node)) return + if (!e.currentTarget.contains(e.target)) return + // Select the pretty-printed code. + const sel = window.getSelection() + if (!sel) return + sel.removeAllRanges() + sel.selectAllChildren(e.currentTarget) + }} + > + {goToDefErrorState && ( + {`No definition found for '${TaggedText_stripTags(fmt)}'`} + )} + {htShouldShow && ( + + + + + + )} + + + ) } From 81d966344a6c1226176944196bedb7817e964c06 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 3 Jul 2024 13:35:31 +0200 Subject: [PATCH 06/26] refactor: conditional rendering for messages --- lean4-infoview/src/infoview/info.tsx | 12 ++++++++---- lean4-infoview/src/infoview/messages.tsx | 19 +++++++++++-------- 2 files changed, 19 insertions(+), 12 deletions(-) diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx index 311ee3e6c..bd9fa7d86 100644 --- a/lean4-infoview/src/infoview/info.tsx +++ b/lean4-infoview/src/infoview/info.tsx @@ -157,6 +157,8 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { [selectedLocs], ) + const [messagesAreOpen, setMessagesAreOpen] = React.useState(true) + /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */ return ( <> @@ -207,11 +209,13 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { else return inner })}
-
+
setMessagesAreOpen(e.currentTarget.open)}> Messages ({messages.length}) -
- -
+ {messagesAreOpen && ( +
+ +
+ )}
{nothingToShow && diff --git a/lean4-infoview/src/infoview/messages.tsx b/lean4-infoview/src/infoview/messages.tsx index 05d1f51a0..868501ddf 100644 --- a/lean4-infoview/src/infoview/messages.tsx +++ b/lean4-infoview/src/infoview/messages.tsx @@ -36,6 +36,7 @@ const MessageView = React.memo(({ uri, diag }: MessageViewProps) => { const fname = escapeHtml(basename(uri)) const { line, character } = diag.range.start const loc: Location = { uri, range: diag.range } + const [messagesAreOpen, setMessagesAreOpen] = React.useState(true) /* We grab the text contents of the message from `node.innerText`. */ const node = React.useRef(null) const severityClass = diag.severity @@ -52,7 +53,7 @@ const MessageView = React.memo(({ uri, diag }: MessageViewProps) => { [uri, diag.fullRange, diag.range], ) return ( -
+
setMessagesAreOpen(e.currentTarget.open)}> {title} e.preventDefault()}> @@ -80,13 +81,15 @@ const MessageView = React.memo(({ uri, diag }: MessageViewProps) => { > -
- 
-                    
-                        
-                    
-
-
+ {messagesAreOpen && ( +
+ 
+                        
+                            
+                        
+
+
+ )}
) }, fastIsEqual) From 9317290b325adb97c7270f8e2437bb32e00b374e Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 3 Jul 2024 17:20:23 +0200 Subject: [PATCH 07/26] refactor: lazily initialize tooltip reference to avoid re-render --- .../src/infoview/interactiveCode.tsx | 52 +++++++++++++------ 1 file changed, 36 insertions(+), 16 deletions(-) diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index 5c741d514..f8303628b 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -148,8 +148,16 @@ const DIFF_TAG_TO_EXPLANATION: { [K in DiffTag]: string } = { function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) { const rs = useRpcSession() const ec = React.useContext(EditorContext) + const htRef = React.useRef(null) const [hoverState, setHoverState] = React.useState('off') - const [goToDefErrorState, setGoToDefErrorState] = React.useState(false) + const [goToDefErrorState, setGoToDefErrorState_] = React.useState(false) + const [goToDefErrorTooltipAnchorRef, setGoToDefErrorTooltipAnchorRef] = React.useState(null) + const setGoToDefErrorState: (isError: boolean) => void = React.useCallback(isError => { + setGoToDefErrorState_(isError) + if (isError) { + setGoToDefErrorTooltipAnchorRef(htRef.current) + } + }, []) // We mimick the VSCode ctrl-hover and ctrl-click UI for go-to-definition const [goToLoc, setGoToLoc] = React.useState(undefined) @@ -179,12 +187,13 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) if (loc === undefined) { if (withError) { setGoToDefErrorState(true) + setGoToDefErrorTooltipAnchorRef(htRef.current) } return } await ec.revealPosition({ uri: loc.uri, ...loc.range.start }) }, - [fetchGoToLoc, ec], + [fetchGoToLoc, ec, setGoToDefErrorState], ) const locs = React.useContext(LocationsContext) @@ -224,8 +233,6 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) ////////////////////////////////////////////////////////////////////////////////////////////////////////// /* DetectHoverSpan */ - const [htRef, setHTRef] = React.useState(null) - const dhOnPointerEvent = (b: boolean, e: React.PointerEvent) => { // It's more composable to let pointer events bubble up rather than to call `stopPropagation`, // but we only want to handle hovers in the innermost component. So we record that the @@ -233,7 +240,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) // The `contains` check ensures that the node hovered over is a child in the DOM // tree and not just a logical React child (see useLogicalDom and // https://reactjs.org/docs/portals.html#event-bubbling-through-portals). - if (htRef && e.target instanceof Node && htRef.contains(e.target)) { + if (htRef.current && e.target instanceof Node && htRef.current.contains(e.target)) { if ('_DetectHoverSpanSeen' in e) return ;(e as any)._DetectHoverSpanSeen = {} if (!b) slSetHoverStateAll('off') @@ -266,7 +273,14 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) // We are pinned when clicked, shown when hovered over, and otherwise hidden. type TooltipState = 'pin' | 'show' | 'hide' - const [htState, setHTState] = React.useState('hide') + const [htState, setHTState_] = React.useState('hide') + const [hoverTooltipAnchorRef, setHoverTooltipAnchorRef] = React.useState(null) + const setHTState: (state: TooltipState) => void = React.useCallback(state => { + setHTState_(state) + if (state !== 'hide') { + setHoverTooltipAnchorRef(htRef.current) + } + }, []) const htShouldShow = htState !== 'hide' const htTipChainCtx = React.useContext(TipChainContext) @@ -280,14 +294,14 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) htTipChainCtx.pinParent() }, }), - [htTipChainCtx], + [htTipChainCtx, setHTState], ) // Note: because tooltips are attached to `document.body`, they are not descendants of the // hoverable area in the DOM tree. Thus the `contains` check fails for elements within tooltip // contents and succeeds for elements within the hoverable. We can use this to distinguish them. - const htIsWithinHoverable = (el: EventTarget) => htRef && el instanceof Node && htRef.contains(el) - const [htLogicalSpanElt, htLogicalDomStorage] = useLogicalDomObserver({ current: htRef }) + const htIsWithinHoverable = (el: EventTarget) => htRef.current && el instanceof Node && htRef.current.contains(el) + const [htLogicalSpanElt, htLogicalDomStorage] = useLogicalDomObserver(htRef) // We use timeouts for debouncing hover events. const htTimeout = React.useRef() @@ -304,7 +318,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) const htOnClick = (e: React.MouseEvent) => { htClearTimeout() - setHTState(state => (state === 'pin' ? 'hide' : 'pin')) + setHTState(htState === 'pin' ? 'hide' : 'pin') e.stopPropagation() } @@ -312,7 +326,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) htClearTimeout() setHTState('hide') setGoToDefErrorState(false) - }, []) + }, [setHTState, setGoToDefErrorState]) useOnClickOutside(htLogicalSpanElt, htOnClickOutside) const htIsPointerOverTooltip = React.useRef(false) @@ -320,14 +334,14 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) htClearTimeout() if (!htConfig.showTooltipOnHover) return htTimeout.current = window.setTimeout(() => { - setHTState(state => (state === 'hide' ? 'show' : state)) + setHTState(htState === 'hide' ? 'show' : htState) htTimeout.current = undefined }, htShowDelay) } const htStartHideTimeout = () => { htClearTimeout() htTimeout.current = window.setTimeout(() => { - if (!htIsPointerOverTooltip.current) setHTState(state => (state === 'show' ? 'hide' : state)) + if (!htIsPointerOverTooltip.current) setHTState(htState === 'show' ? 'hide' : htState) htTimeout.current = undefined }, htHideDelay) } @@ -355,7 +369,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) return ( ) }} > {goToDefErrorState && ( - {`No definition found for '${TaggedText_stripTags(fmt)}'`} + {`No definition found for '${TaggedText_stripTags(fmt)}'`} )} {htShouldShow && ( - + From cc863ac364fbd5bfbbddc2eabf1535d3a8b7d485 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 4 Jul 2024 16:23:56 +0200 Subject: [PATCH 08/26] refactor: eliminate redundant re-render --- lean4-infoview/src/infoview/info.tsx | 89 ++++++++++++++---------- lean4-infoview/src/infoview/messages.tsx | 21 +++--- 2 files changed, 61 insertions(+), 49 deletions(-) diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx index bd9fa7d86..0a45e75ad 100644 --- a/lean4-infoview/src/infoview/info.tsx +++ b/lean4-infoview/src/infoview/info.tsx @@ -15,6 +15,7 @@ import { UserWidgetInstance, Widget_getWidgets, } from '@leanprover/infoview-api' +import { Details } from './collapsing' import { ConfigContext, EditorContext, EnvPosContext, LspDiagnosticsContext, ProgressContext } from './contexts' import { GoalsLocation, Locations, LocationsContext } from './goalLocation' import { FilteredGoals, goalsToString } from './goals' @@ -116,28 +117,19 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => { ) }) -interface InfoDisplayContentProps extends PausableProps { +interface GoalInfoDisplayProps { pos: DocumentPosition - messages: InteractiveDiagnostic[] goals?: InteractiveGoals termGoal?: InteractiveTermGoal - error?: string userWidgets: UserWidgetInstance[] - triggerUpdate: () => Promise } -const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { - const { pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused } = props +function GoalInfoDisplay(props: GoalInfoDisplayProps) { + const { pos, goals, termGoal, userWidgets } = props - 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 - const [selectedLocs, setSelectedLocs] = React.useState([]) - React.useEffect(() => setSelectedLocs([]), [pos.uri, pos.line, pos.character]) const locs: Locations = React.useMemo( () => ({ @@ -157,26 +149,8 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { [selectedLocs], ) - const [messagesAreOpen, setMessagesAreOpen] = React.useState(true) - - /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */ return ( <> - {hasError && ( - - )} @@ -208,15 +182,56 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { ) else return inner })} + + ) +} + +interface InfoDisplayContentProps extends GoalInfoDisplayProps, PausableProps { + messages: InteractiveDiagnostic[] + error?: string + triggerUpdate: () => Promise +} + +const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { + const { pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused } = props + + const hasWidget = userWidgets.length > 0 + const hasError = !!error + const hasMessages = messages.length !== 0 + const nothingToShow = !hasError && !goals && !termGoal && !hasMessages && !hasWidget + + /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */ + return ( + <> + {hasError && ( + + )} +
-
setMessagesAreOpen(e.currentTarget.open)}> +
Messages ({messages.length}) - {messagesAreOpen && ( -
- -
- )} -
+
+ +
+
{nothingToShow && (isPaused ? ( diff --git a/lean4-infoview/src/infoview/messages.tsx b/lean4-infoview/src/infoview/messages.tsx index 868501ddf..96e06a7d6 100644 --- a/lean4-infoview/src/infoview/messages.tsx +++ b/lean4-infoview/src/infoview/messages.tsx @@ -36,7 +36,6 @@ const MessageView = React.memo(({ uri, diag }: MessageViewProps) => { const fname = escapeHtml(basename(uri)) const { line, character } = diag.range.start const loc: Location = { uri, range: diag.range } - const [messagesAreOpen, setMessagesAreOpen] = React.useState(true) /* We grab the text contents of the message from `node.innerText`. */ const node = React.useRef(null) const severityClass = diag.severity @@ -53,7 +52,7 @@ const MessageView = React.memo(({ uri, diag }: MessageViewProps) => { [uri, diag.fullRange, diag.range], ) return ( -
setMessagesAreOpen(e.currentTarget.open)}> +
{title} e.preventDefault()}> @@ -81,16 +80,14 @@ const MessageView = React.memo(({ uri, diag }: MessageViewProps) => { > - {messagesAreOpen && ( -
- 
-                        
-                            
-                        
-
-
- )} -
+
+ 
+                    
+                        
+                    
+
+
+
) }, fastIsEqual) From a6da37ede320764f16dde34e1f0ed5b20e20b775 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 4 Jul 2024 17:52:45 +0200 Subject: [PATCH 09/26] fix: hover bug introduced in previous refactoring --- lean4-infoview/src/infoview/interactiveCode.tsx | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index f8303628b..13127bae3 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -218,9 +218,8 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) ////////////////////////////////////////////////////////////////////////////////////////////////////////// /* SelectableLocation */ - const [slHoverState, setSLHoverState] = React.useState('off') let slSpanClassName: string = '' - if (slHoverState !== 'off') { + if (hoverState !== 'off') { slSpanClassName += 'highlight ' } else if (isSelected) { slSpanClassName += 'highlight-selected ' @@ -228,7 +227,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) slSpanClassName += spanClassName const slSetHoverStateAll: React.Dispatch> = React.useCallback(val => { - setSLHoverState(val) + setHoverState(val) }, []) ////////////////////////////////////////////////////////////////////////////////////////////////////////// From c76c390a7a8ed60338a104727b922448da1bbfbd Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 4 Jul 2024 18:04:39 +0200 Subject: [PATCH 10/26] refactor: eliminate extremely slow effect --- .../src/infoview/interactiveCode.tsx | 26 ++++++------------- 1 file changed, 8 insertions(+), 18 deletions(-) diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index 13127bae3..4440a2568 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -248,24 +248,6 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) } } - React.useEffect(() => { - const onKeyDown = (e: KeyboardEvent) => { - if (e.key === 'Control' || e.key === 'Meta') slSetHoverStateAll(st => (st === 'over' ? 'ctrlOver' : st)) - } - - const onKeyUp = (e: KeyboardEvent) => { - if (e.key === 'Control' || e.key === 'Meta') slSetHoverStateAll(st => (st === 'ctrlOver' ? 'over' : st)) - } - - // Note: In VSCode these events do not fire when the webview is not in focus. - document.addEventListener('keydown', onKeyDown) - document.addEventListener('keyup', onKeyUp) - return () => { - document.removeEventListener('keydown', onKeyDown) - document.removeEventListener('keyup', onKeyUp) - } - }, [slSetHoverStateAll]) - ////////////////////////////////////////////////////////////////////////////////////////////////////////// /* WithTooltipOnHover */ const htConfig = React.useContext(ConfigContext) @@ -408,6 +390,14 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) if (e.ctrlKey || e.metaKey) slSetHoverStateAll(st => (st === 'over' ? 'ctrlOver' : st)) else slSetHoverStateAll(st => (st === 'ctrlOver' ? 'over' : st)) }} + onKeyDown={e => { + if (e.key === 'Control' || e.key === 'Meta') + slSetHoverStateAll(st => (st === 'over' ? 'ctrlOver' : st)) + }} + onKeyUp={e => { + if (e.key === 'Control' || e.key === 'Meta') + slSetHoverStateAll(st => (st === 'ctrlOver' ? 'over' : st)) + }} onContextMenu={e => { // Mark the event as seen so that parent handlers skip it. // We cannot use `stopPropagation` as that prevents the VSC context menu from showing up. From a2e7e9c9ed86f6934631a5fa2867cf1e246cf36d Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 5 Jul 2024 10:57:38 +0200 Subject: [PATCH 11/26] refactor: fix last remaining effect performance bottleneck --- lean4-infoview/src/infoview/interactiveCode.tsx | 2 +- lean4-infoview/src/infoview/util.ts | 11 +++++++++-- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index 4440a2568..3872f7ef7 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -308,7 +308,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) setHTState('hide') setGoToDefErrorState(false) }, [setHTState, setGoToDefErrorState]) - useOnClickOutside(htLogicalSpanElt, htOnClickOutside) + useOnClickOutside(htLogicalSpanElt, htOnClickOutside, htShouldShow) const htIsPointerOverTooltip = React.useRef(false) const htStartShowTimeout = () => { diff --git a/lean4-infoview/src/infoview/util.ts b/lean4-infoview/src/infoview/util.ts index 0028d71a6..30b96f3e6 100644 --- a/lean4-infoview/src/infoview/util.ts +++ b/lean4-infoview/src/infoview/util.ts @@ -288,8 +288,15 @@ export function useLogicalDomObserver(elt: React.RefObject): [Logic * An effect which calls `onClickOutside` whenever an element not logically descending from `ld` * (see {@link useLogicalDomObserver}) is clicked. Note that `onClickOutside` is not called on clicks * on the scrollbar since these should usually not impact the app's state. */ -export function useOnClickOutside(ld: LogicalDomElement, onClickOutside: (_: PointerEvent) => void) { +export function useOnClickOutside( + ld: LogicalDomElement, + onClickOutside: (_: PointerEvent) => void, + trigger: boolean = true, +) { React.useEffect(() => { + if (!trigger) { + return + } const onClickAnywhere = (e: PointerEvent) => { if (e.target instanceof Node && !ld.contains(e.target)) { if (e.target instanceof Element && e.target.tagName === 'HTML') { @@ -301,7 +308,7 @@ export function useOnClickOutside(ld: LogicalDomElement, onClickOutside: (_: Poi document.addEventListener('pointerdown', onClickAnywhere) return () => document.removeEventListener('pointerdown', onClickAnywhere) - }, [ld, onClickOutside]) + }, [ld, onClickOutside, trigger]) } /** Sends an exception object to a throwable error. From c9ea2f907b7b380d58cbd01b562df9f00f888f27 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 5 Jul 2024 11:47:50 +0200 Subject: [PATCH 12/26] refactor: avoid redundant hover re-renders --- lean4-infoview/src/infoview/interactiveCode.tsx | 16 +++++++++++++--- lean4-infoview/src/infoview/util.ts | 5 +++++ 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index 3872f7ef7..fb30acbed 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -15,7 +15,15 @@ import { ConfigContext, EditorContext } from './contexts' import { GoalsLocation, LocationsContext } from './goalLocation' import { useRpcSession } from './rpcSessions' import { HoverState, TipChainContext, Tooltip } from './tooltips' -import { LogicalDomContext, mapRpcError, useAsync, useEvent, useLogicalDomObserver, useOnClickOutside } from './util' +import { + genericMemo, + LogicalDomContext, + mapRpcError, + useAsync, + useEvent, + useLogicalDomObserver, + useOnClickOutside, +} from './util' export interface InteractiveTextComponentProps { fmt: TaggedText @@ -47,6 +55,8 @@ export function InteractiveTaggedText({ fmt, InnerTagUi }: InteractiveTaggedT else throw new Error(`malformed 'TaggedText': '${fmt}'`) } +export const MemoedInteractiveTaggedText = genericMemo(InteractiveTaggedText) + interface TypePopupContentsProps { info: SubexprInfo } @@ -428,7 +438,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) )} - + ) @@ -440,7 +450,7 @@ export type InteractiveCodeProps = InteractiveTextComponentProps export function InteractiveCode(props: InteractiveCodeProps) { return ( - + ) } diff --git a/lean4-infoview/src/infoview/util.ts b/lean4-infoview/src/infoview/util.ts index 30b96f3e6..fecffc83a 100644 --- a/lean4-infoview/src/infoview/util.ts +++ b/lean4-infoview/src/infoview/util.ts @@ -424,3 +424,8 @@ export function useAsyncPersistent(fn: () => Promise, deps: React.Dependen } return state } + +/** + * Memoizes a generic component in a way that does not require a type cast. + */ +export const genericMemo: (component: T) => T = React.memo From ac4675cfc135ac4eb0270e5411b3a8b17a7d2307 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Mon, 8 Jul 2024 17:48:28 +0200 Subject: [PATCH 13/26] refactor: use custom hook for selectable location --- lean4-infoview/src/infoview/goalLocation.tsx | 155 +++++++++++------- lean4-infoview/src/infoview/goals.tsx | 76 +++++++-- lean4-infoview/src/infoview/index.css | 2 +- .../src/infoview/interactiveCode.tsx | 103 +++++------- lean4-infoview/src/infoview/tooltips.tsx | 69 -------- 5 files changed, 199 insertions(+), 206 deletions(-) diff --git a/lean4-infoview/src/infoview/goalLocation.tsx b/lean4-infoview/src/infoview/goalLocation.tsx index 3c5b8d43d..18ccdf4c2 100644 --- a/lean4-infoview/src/infoview/goalLocation.tsx +++ b/lean4-infoview/src/infoview/goalLocation.tsx @@ -5,7 +5,7 @@ Authors: E.W.Ayers, Wojciech Nawrocki */ import { FVarId, MVarId, SubexprPos } from '@leanprover/infoview-api' import * as React from 'react' -import { DetectHoverSpan, HoverState } from './tooltips' +import { HoverState } from './tooltips' /** * A location within a goal. It is either: @@ -76,66 +76,107 @@ export interface Locations { export const LocationsContext = React.createContext(undefined) -type SelectableLocationProps = React.PropsWithoutRef< - React.DetailedHTMLProps, HTMLSpanElement> -> & { - locs?: Locations - loc?: GoalsLocation - alwaysHighlight: boolean - setHoverState?: React.Dispatch> +export type HoverSettings = { highlightOnHover: true } | { highlightOnHover: false } +export type ModHoverSettings = { highlightOnModHover: true } | { highlightOnModHover: false } +export type SelectionSettings = { highlightOnSelection: true; loc: GoalsLocation } | { highlightOnSelection: false } +export interface LocationHighlightSettings { + ref: React.RefObject + hoverSettings: HoverSettings + modHoverSettings: ModHoverSettings + selectionSettings: SelectionSettings +} +export interface HighlightedLocation { + hoverState: HoverState + setHoverState: React.Dispatch> + className: string + onPointerEvent: (b: boolean, e: React.PointerEvent) => void + onPointerMove: (e: React.PointerEvent) => void + onKeyDown: (e: React.KeyboardEvent) => void + onKeyUp: (e: React.KeyboardEvent) => void + onClick: (e: React.MouseEvent) => boolean + onPointerDown: (e: React.PointerEvent) => void } /** - * A `` with a corresponding {@link GoalsLocation} which can be (un)selected using shift-click. - * If `locs` or `loc` is `undefined`, selection functionality is turned off. The element is also - * highlighted when hovered over if `alwaysHighlight` is `true` or `locs` and `loc` are both defined. - * `setHoverState` is passed through to {@link DetectHoverSpan}. */ -export function SelectableLocation(props_: SelectableLocationProps): JSX.Element { - const { locs, loc, alwaysHighlight, setHoverState: setParentHoverState, ...props } = props_ - - const shouldHighlight: boolean = alwaysHighlight || (!!locs && !!loc) + * Logic for a `` with a corresponding {@link GoalsLocation} which can be (un)selected using shift-click. + */ +export function useHighlightedLocation(settings: LocationHighlightSettings): HighlightedLocation { + const { ref, hoverSettings, modHoverSettings, selectionSettings } = settings + const [hoverState, setHoverState] = React.useState('off') - let spanClassName: string = '' - if (shouldHighlight) { - spanClassName += 'highlightable ' - if (hoverState !== 'off') spanClassName += 'highlight ' - if (props.className) spanClassName += props.className + + const locs = React.useContext(LocationsContext) + let className: string = '' + if (hoverSettings.highlightOnHover && hoverState !== 'off') { + className += 'highlight ' + } else if (selectionSettings.highlightOnSelection && locs && locs.isSelected(selectionSettings.loc)) { + className += 'highlight-selected ' + } + if (modHoverSettings.highlightOnModHover && hoverState === 'ctrlOver') { + className += 'underline ' } - const innerSpanClassName: string = - 'highlightable ' + (locs && loc && locs.isSelected(loc) ? 'highlight-selected ' : '') - - const setHoverStateAll: React.Dispatch> = React.useCallback( - val => { - setHoverState(val) - if (setParentHoverState) setParentHoverState(val) - }, - [setParentHoverState], - ) - - return ( - { - // On shift-click, if we are in a context where selecting subexpressions makes sense, - // (un)select the current subexpression. - if (e.shiftKey && locs && loc) { - locs.setSelected(loc, on => !on) - e.stopPropagation() - } - if (props.onClick) props.onClick(e) - }} - onPointerDown={e => { - // Since shift-click on this component is a custom selection, when shift is held prevent - // the default action which on text is to start a text selection. - if (e.shiftKey) e.preventDefault() - if (props.onPointerDown) props.onPointerDown(e) - }} - > - {/* Note: we use two spans so that the two `highlight`s don't interfere. */} - {props.children} - - ) + const onPointerEvent = (b: boolean, e: React.PointerEvent) => { + // It's more composable to let pointer events bubble up rather than to call `stopPropagation`, + // but we only want to handle hovers in the innermost component. So we record that the + // event was handled with a property. + // The `contains` check ensures that the node hovered over is a child in the DOM + // tree and not just a logical React child (see useLogicalDom and + // https://reactjs.org/docs/portals.html#event-bubbling-through-portals). + if (ref.current && e.target instanceof Node && ref.current.contains(e.target)) { + if ('_DetectHoverSpanSeen' in e) return + ;(e as any)._DetectHoverSpanSeen = {} + if (!b) setHoverState('off') + else if (e.ctrlKey || e.metaKey) setHoverState('ctrlOver') + else setHoverState('over') + } + } + + const onPointerMove = (e: React.PointerEvent) => { + if (e.ctrlKey || e.metaKey) setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) + else setHoverState(st => (st === 'ctrlOver' ? 'over' : st)) + } + + const onKeyDown = (e: React.KeyboardEvent) => { + if (e.key === 'Control' || e.key === 'Meta') { + setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) + } + } + + const onKeyUp = (e: React.KeyboardEvent) => { + if (e.key === 'Control' || e.key === 'Meta') { + setHoverState(st => (st === 'ctrlOver' ? 'over' : st)) + } + } + + const onClick = (e: React.MouseEvent) => { + // On shift-click, if we are in a context where selecting subexpressions makes sense, + // (un)select the current subexpression. + if (selectionSettings.highlightOnSelection && locs && e.shiftKey) { + locs.setSelected(selectionSettings.loc, on => !on) + e.stopPropagation() + return true + } + return false + } + + const onPointerDown = (e: React.PointerEvent) => { + // We have special handling for shift+click events, so prevent default browser + // events from interfering when shift is held. + if (selectionSettings.highlightOnSelection && locs && e.shiftKey) { + e.preventDefault() + } + } + + return { + hoverState, + setHoverState, + className, + onPointerEvent, + onPointerMove, + onKeyDown, + onKeyUp, + onClick, + onPointerDown, + } } diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx index 27024b62a..823569614 100644 --- a/lean4-infoview/src/infoview/goals.tsx +++ b/lean4-infoview/src/infoview/goals.tsx @@ -10,7 +10,7 @@ import { import * as React from 'react' import { Details } from './collapsing' import { ConfigContext, EditorContext } from './contexts' -import { Locations, LocationsContext, SelectableLocation } from './goalLocation' +import { Locations, LocationsContext, SelectionSettings, useHighlightedLocation } from './goalLocation' import { InteractiveCode } from './interactiveCode' import { WithTooltipOnHover } from './tooltips' import { useEvent } from './util' @@ -74,6 +74,60 @@ function getFilteredHypotheses( }, []) } +interface HypNameProps { + name: string + isInserted: boolean + isRemoved: boolean + mvarId?: string | undefined + fvarId?: string | undefined + key: number +} + +function HypName({ name, isInserted, isRemoved, mvarId, fvarId, key }: HypNameProps) { + const ref = React.useRef(null) + + let selectionSettings: SelectionSettings + if (mvarId !== undefined && fvarId !== undefined) { + selectionSettings = { highlightOnSelection: true, loc: { mvarId, loc: { hyp: fvarId } } } + } else { + selectionSettings = { highlightOnSelection: false } + } + + const locs = React.useContext(LocationsContext) + + const hl = useHighlightedLocation({ + ref, + hoverSettings: { highlightOnHover: locs !== undefined && mvarId !== undefined && fvarId !== undefined }, + modHoverSettings: { highlightOnModHover: false }, + selectionSettings, + }) + + const namecls: string = + (isInserted ? 'inserted-text ' : '') + + (isRemoved ? 'removed-text ' : '') + + (isInaccessibleName(name) ? 'goal-inaccessible ' : '') + + hl.className + return ( + <> + hl.onPointerEvent(true, e)} + onPointerOut={e => hl.onPointerEvent(false, e)} + onPointerMove={e => hl.onPointerMove(e)} + onKeyDown={e => hl.onKeyDown(e)} + onKeyUp={e => hl.onKeyUp(e)} + onClick={e => hl.onClick(e)} + onPointerDown={e => hl.onPointerDown(e)} + > + {name} + +   + + ) +} + interface HypProps { hyp: InteractiveHypothesisBundle mvarId?: MVarId @@ -82,19 +136,15 @@ interface HypProps { function Hyp({ hyp: h, mvarId }: HypProps) { const locs = React.useContext(LocationsContext) - const namecls: string = (h.isInserted ? 'inserted-text ' : '') + (h.isRemoved ? 'removed-text ' : '') - const names = InteractiveHypothesisBundle_nonAnonymousNames(h).map((n, i) => ( - - i ? { mvarId, loc: { hyp: h.fvarIds[i] } } : undefined} - alwaysHighlight={false} - > - {n} - -   - + )) const typeLocs: Locations | undefined = React.useMemo( diff --git a/lean4-infoview/src/infoview/index.css b/lean4-infoview/src/infoview/index.css index ec8f3512b..e16f2314b 100644 --- a/lean4-infoview/src/infoview/index.css +++ b/lean4-infoview/src/infoview/index.css @@ -54,7 +54,7 @@ body { } .highlight-selected { - background-color: var(--vscode-editorOverviewRuler-rangeHighlightForeground); + background-color: var(--vscode-editorOverviewRuler-rangeHighlightForeground) !important; } /* Interactive traces */ diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index fb30acbed..e66333e2b 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -12,9 +12,9 @@ import { import { marked } from 'marked' import { Location } from 'vscode-languageserver-protocol' import { ConfigContext, EditorContext } from './contexts' -import { GoalsLocation, LocationsContext } from './goalLocation' +import { GoalsLocation, LocationsContext, SelectionSettings, useHighlightedLocation } from './goalLocation' import { useRpcSession } from './rpcSessions' -import { HoverState, TipChainContext, Tooltip } from './tooltips' +import { TipChainContext, Tooltip } from './tooltips' import { genericMemo, LogicalDomContext, @@ -159,7 +159,10 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) const rs = useRpcSession() const ec = React.useContext(EditorContext) const htRef = React.useRef(null) - const [hoverState, setHoverState] = React.useState('off') + + // We mimick the VSCode ctrl-hover and ctrl-click UI for go-to-definition + const [goToLoc, setGoToLoc] = React.useState(undefined) + const [goToDefErrorState, setGoToDefErrorState_] = React.useState(false) const [goToDefErrorTooltipAnchorRef, setGoToDefErrorTooltipAnchorRef] = React.useState(null) const setGoToDefErrorState: (isError: boolean) => void = React.useCallback(isError => { @@ -169,8 +172,25 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) } }, []) - // We mimick the VSCode ctrl-hover and ctrl-click UI for go-to-definition - const [goToLoc, setGoToLoc] = React.useState(undefined) + const locs = React.useContext(LocationsContext) + let selectionSettings: SelectionSettings + if (locs && locs.subexprTemplate && ct.subexprPos) { + selectionSettings = { + highlightOnSelection: true, + loc: GoalsLocation.withSubexprPos(locs.subexprTemplate, ct.subexprPos), + } + } else { + selectionSettings = { highlightOnSelection: false } + } + + const hl = useHighlightedLocation({ + ref: htRef, + hoverSettings: { highlightOnHover: true }, + modHoverSettings: { highlightOnModHover: goToLoc !== undefined }, + selectionSettings, + }) + const [hoverState, setHoverState] = [hl.hoverState, hl.setHoverState] + const fetchGoToLoc = React.useCallback(async () => { if (goToLoc !== undefined) return goToLoc try { @@ -185,6 +205,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) } return undefined }, [rs, ct.info, goToLoc]) + // Eagerly fetch the location as soon as the pointer enters this area so that we can show // an underline if a jump target is available. React.useEffect(() => { @@ -206,16 +227,9 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) [fetchGoToLoc, ec, setGoToDefErrorState], ) - const locs = React.useContext(LocationsContext) - const ourLoc = - locs && locs.subexprTemplate && ct.subexprPos - ? GoalsLocation.withSubexprPos(locs.subexprTemplate, ct.subexprPos) - : undefined - const isSelected = locs && ourLoc && locs.isSelected(ourLoc) - - let spanClassName: string = hoverState === 'ctrlOver' && goToLoc !== undefined ? 'underline ' : '' + let className = hl.className if (ct.diffStatus) { - spanClassName += DIFF_TAG_TO_CLASS[ct.diffStatus] + ' ' + className += DIFF_TAG_TO_CLASS[ct.diffStatus] + ' ' } // ID that we can use to identify the component that a context menu was opened in. @@ -226,38 +240,6 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) const vscodeContext = { interactiveCodeTagId } useEvent(ec.events.goToDefinition, async _ => void execGoToLoc(true), [execGoToLoc], interactiveCodeTagId) - ////////////////////////////////////////////////////////////////////////////////////////////////////////// - /* SelectableLocation */ - let slSpanClassName: string = '' - if (hoverState !== 'off') { - slSpanClassName += 'highlight ' - } else if (isSelected) { - slSpanClassName += 'highlight-selected ' - } - slSpanClassName += spanClassName - - const slSetHoverStateAll: React.Dispatch> = React.useCallback(val => { - setHoverState(val) - }, []) - - ////////////////////////////////////////////////////////////////////////////////////////////////////////// - /* DetectHoverSpan */ - const dhOnPointerEvent = (b: boolean, e: React.PointerEvent) => { - // It's more composable to let pointer events bubble up rather than to call `stopPropagation`, - // but we only want to handle hovers in the innermost component. So we record that the - // event was handled with a property. - // The `contains` check ensures that the node hovered over is a child in the DOM - // tree and not just a logical React child (see useLogicalDom and - // https://reactjs.org/docs/portals.html#event-bubbling-through-portals). - if (htRef.current && e.target instanceof Node && htRef.current.contains(e.target)) { - if ('_DetectHoverSpanSeen' in e) return - ;(e as any)._DetectHoverSpanSeen = {} - if (!b) slSetHoverStateAll('off') - else if (e.ctrlKey || e.metaKey) slSetHoverStateAll('ctrlOver') - else slSetHoverStateAll('over') - } - } - ////////////////////////////////////////////////////////////////////////////////////////////////////////// /* WithTooltipOnHover */ const htConfig = React.useContext(ConfigContext) @@ -361,15 +343,12 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) { - // On shift-click, if we are in a context where selecting subexpressions makes sense, - // (un)select the current subexpression. - if (e.shiftKey && locs && ourLoc) { - locs.setSelected(ourLoc, on => !on) - e.stopPropagation() + const stopClick = hl.onClick(e) + if (stopClick) { return } htGuardMouseEvent(e => { @@ -382,32 +361,24 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) if (!window.getSelection()?.toString()) setGoToDefErrorState(false) }} onPointerDown={e => { + hl.onPointerDown(e) // We have special handling for some modifier+click events, so prevent default browser // events from interfering when a modifier is held. if (htIsModifierHeld(e)) e.preventDefault() }} onPointerOver={e => { - dhOnPointerEvent(true, e) + hl.onPointerEvent(true, e) if (!htIsModifierHeld(e)) { htGuardMouseEvent(_ => htStartShowTimeout(), e) } }} onPointerOut={e => { - dhOnPointerEvent(false, e) + hl.onPointerEvent(false, e) htGuardMouseEvent(_ => htStartHideTimeout(), e) }} - onPointerMove={e => { - if (e.ctrlKey || e.metaKey) slSetHoverStateAll(st => (st === 'over' ? 'ctrlOver' : st)) - else slSetHoverStateAll(st => (st === 'ctrlOver' ? 'over' : st)) - }} - onKeyDown={e => { - if (e.key === 'Control' || e.key === 'Meta') - slSetHoverStateAll(st => (st === 'over' ? 'ctrlOver' : st)) - }} - onKeyUp={e => { - if (e.key === 'Control' || e.key === 'Meta') - slSetHoverStateAll(st => (st === 'ctrlOver' ? 'over' : st)) - }} + onPointerMove={e => hl.onPointerMove(e)} + onKeyDown={e => hl.onKeyDown(e)} + onKeyUp={e => hl.onKeyUp(e)} onContextMenu={e => { // Mark the event as seen so that parent handlers skip it. // We cannot use `stopPropagation` as that prevents the VSC context menu from showing up. diff --git a/lean4-infoview/src/infoview/tooltips.tsx b/lean4-infoview/src/infoview/tooltips.tsx index ce6f7523c..7e741e572 100644 --- a/lean4-infoview/src/infoview/tooltips.tsx +++ b/lean4-infoview/src/infoview/tooltips.tsx @@ -113,75 +113,6 @@ export function WithToggleableTooltip(props_: WithToggleableTooltipProps) { */ export type HoverState = 'off' | 'over' | 'ctrlOver' -export type DetectHoverSpanProps = React.DetailedHTMLProps, HTMLSpanElement> & { - setHoverState: React.Dispatch> -} - -/** An element which calls `setHoverState` when the hover state of its DOM children changes. - * - * It is implemented with JS rather than CSS in order to allow nesting of these elements. When nested, - * only the smallest (deepest in the DOM tree) {@link DetectHoverSpan} has an enabled hover state. */ -export function DetectHoverSpan(props_: DetectHoverSpanProps) { - const { setHoverState, ...props } = props_ - const ref = React.useRef(null) - - const onPointerEvent = (b: boolean, e: React.PointerEvent) => { - // It's more composable to let pointer events bubble up rather than to call `stopPropagation`, - // but we only want to handle hovers in the innermost component. So we record that the - // event was handled with a property. - // The `contains` check ensures that the node hovered over is a child in the DOM - // tree and not just a logical React child (see useLogicalDom and - // https://reactjs.org/docs/portals.html#event-bubbling-through-portals). - if (ref.current && e.target instanceof Node && ref.current.contains(e.target)) { - if ('_DetectHoverSpanSeen' in e) return - ;(e as any)._DetectHoverSpanSeen = {} - if (!b) setHoverState('off') - else if (e.ctrlKey || e.metaKey) setHoverState('ctrlOver') - else setHoverState('over') - } - } - - React.useEffect(() => { - const onKeyDown = (e: KeyboardEvent) => { - if (e.key === 'Control' || e.key === 'Meta') setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) - } - - const onKeyUp = (e: KeyboardEvent) => { - if (e.key === 'Control' || e.key === 'Meta') setHoverState(st => (st === 'ctrlOver' ? 'over' : st)) - } - - // Note: In VSCode these events do not fire when the webview is not in focus. - document.addEventListener('keydown', onKeyDown) - document.addEventListener('keyup', onKeyUp) - return () => { - document.removeEventListener('keydown', onKeyDown) - document.removeEventListener('keyup', onKeyUp) - } - }, [setHoverState]) - - return ( - { - onPointerEvent(true, e) - if (props.onPointerOver) props.onPointerOver(e) - }} - onPointerOut={e => { - onPointerEvent(false, e) - if (props.onPointerOut) props.onPointerOut(e) - }} - onPointerMove={e => { - if (e.ctrlKey || e.metaKey) setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) - else setHoverState(st => (st === 'ctrlOver' ? 'over' : st)) - if (props.onPointerMove) props.onPointerMove(e) - }} - > - {props.children} - - ) -} - /** Pinning a child tooltip has to also pin all ancestors. This context supports that. */ export interface TipChainContext { pinParent(): void From 6108ec4d0bce27a42a9f40ec2adead48d3c3af92 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 9 Jul 2024 13:57:59 +0200 Subject: [PATCH 14/26] refactor: use custom hook for toggleable tooltip --- .../src/infoview/interactiveCode.tsx | 39 +++++------- lean4-infoview/src/infoview/tooltips.tsx | 62 +++++++++++-------- 2 files changed, 52 insertions(+), 49 deletions(-) diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index e66333e2b..d62223f43 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -14,7 +14,7 @@ import { Location } from 'vscode-languageserver-protocol' import { ConfigContext, EditorContext } from './contexts' import { GoalsLocation, LocationsContext, SelectionSettings, useHighlightedLocation } from './goalLocation' import { useRpcSession } from './rpcSessions' -import { TipChainContext, Tooltip } from './tooltips' +import { TipChainContext, Tooltip, useToggleableTooltip } from './tooltips' import { genericMemo, LogicalDomContext, @@ -160,18 +160,17 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) const ec = React.useContext(EditorContext) const htRef = React.useRef(null) + const [htLogicalSpanElt, htLogicalDomStorage] = useLogicalDomObserver(htRef) + + const tt = useToggleableTooltip(htRef, <>{`No definition found for '${TaggedText_stripTags(fmt)}'`}) + const [setGoToDefErrorTooltipDisplayed, onClickOutsideGoToDefErrorTooltip] = [ + tt.setTooltipDisplayed, + tt.onClickOutside, + ] + // We mimick the VSCode ctrl-hover and ctrl-click UI for go-to-definition const [goToLoc, setGoToLoc] = React.useState(undefined) - const [goToDefErrorState, setGoToDefErrorState_] = React.useState(false) - const [goToDefErrorTooltipAnchorRef, setGoToDefErrorTooltipAnchorRef] = React.useState(null) - const setGoToDefErrorState: (isError: boolean) => void = React.useCallback(isError => { - setGoToDefErrorState_(isError) - if (isError) { - setGoToDefErrorTooltipAnchorRef(htRef.current) - } - }, []) - const locs = React.useContext(LocationsContext) let selectionSettings: SelectionSettings if (locs && locs.subexprTemplate && ct.subexprPos) { @@ -217,14 +216,13 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) const loc = await fetchGoToLoc() if (loc === undefined) { if (withError) { - setGoToDefErrorState(true) - setGoToDefErrorTooltipAnchorRef(htRef.current) + setGoToDefErrorTooltipDisplayed(true) } return } await ec.revealPosition({ uri: loc.uri, ...loc.range.start }) }, - [fetchGoToLoc, ec, setGoToDefErrorState], + [fetchGoToLoc, ec, setGoToDefErrorTooltipDisplayed], ) let className = hl.className @@ -274,7 +272,6 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) // hoverable area in the DOM tree. Thus the `contains` check fails for elements within tooltip // contents and succeeds for elements within the hoverable. We can use this to distinguish them. const htIsWithinHoverable = (el: EventTarget) => htRef.current && el instanceof Node && htRef.current.contains(el) - const [htLogicalSpanElt, htLogicalDomStorage] = useLogicalDomObserver(htRef) // We use timeouts for debouncing hover events. const htTimeout = React.useRef() @@ -298,9 +295,9 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) const htOnClickOutside = React.useCallback(() => { htClearTimeout() setHTState('hide') - setGoToDefErrorState(false) - }, [setHTState, setGoToDefErrorState]) - useOnClickOutside(htLogicalSpanElt, htOnClickOutside, htShouldShow) + onClickOutsideGoToDefErrorTooltip() + }, [setHTState, onClickOutsideGoToDefErrorTooltip]) + useOnClickOutside(htLogicalSpanElt, htOnClickOutside, tt.tooltipDisplayed || htShouldShow) const htIsPointerOverTooltip = React.useRef(false) const htStartShowTimeout = () => { @@ -358,7 +355,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) void execGoToLoc(false) } else if (!e.shiftKey) htOnClick(e) }, e) - if (!window.getSelection()?.toString()) setGoToDefErrorState(false) + tt.onClick() }} onPointerDown={e => { hl.onPointerDown(e) @@ -393,11 +390,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) sel.selectAllChildren(e.currentTarget) }} > - {goToDefErrorState && ( - {`No definition found for '${TaggedText_stripTags(fmt)}'`} - )} + {tt.tooltip} {htShouldShow && ( & { - isTooltipShown: boolean - hideTooltip: () => void - tooltipChildren: React.ReactNode +export interface ToggleableTooltip { + tooltip: JSX.Element + tooltipDisplayed: boolean + setTooltipDisplayed: (tooltipDisplayed: boolean) => void + onClick: () => void + onClickOutside: () => void } -export function WithToggleableTooltip(props_: WithToggleableTooltipProps) { - const { isTooltipShown, hideTooltip, tooltipChildren, ...props } = props_ - const [ref, setRef] = React.useState(null) +export function useToggleableTooltip( + ref: React.RefObject, + tooltipChildren: React.ReactNode, +): ToggleableTooltip { + const [anchor, setAnchor] = React.useState(null) + const [tooltipDisplayed, setTooltipDisplayed_] = React.useState(false) + const setTooltipDisplayed = (tooltipDisplayed: boolean) => { + setTooltipDisplayed_(tooltipDisplayed) + if (tooltipDisplayed) { + setAnchor(ref.current) + } + } // Since we do not want to hide the tooltip if the user is trying to select text in it, // we need both the "click outside" and "click inside" handlers here because they @@ -84,26 +95,25 @@ export function WithToggleableTooltip(props_: WithToggleableTooltipProps) { // selections, whereas React ensures that only a selection in the tooltip itself can block // the inside click handler from hiding the tooltip, since the outer selection is removed // before the inside click handler fires. - const [logicalSpanElt, logicalDomStorage] = useLogicalDomObserver({ current: ref }) - const onClickOutside = React.useCallback(() => { - hideTooltip() - }, [hideTooltip]) - useOnClickOutside(logicalSpanElt, onClickOutside) + const onClickOutside = () => { + setTooltipDisplayed(false) + } - return ( - - { - if (!window.getSelection()?.toString()) hideTooltip() - }} - {...props} - > - {isTooltipShown && {tooltipChildren}} - {props.children} - - - ) + const onClick = () => { + if (!window.getSelection()?.toString()) { + setTooltipDisplayed(false) + } + } + + const tooltip = <>{tooltipDisplayed && {tooltipChildren}} + + return { + tooltip, + tooltipDisplayed, + setTooltipDisplayed, + onClick, + onClickOutside, + } } /** Hover state of an element. The pointer can be From 8abaeb3c9fff1179fa45dcafa495b07f1368a87b Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 9 Jul 2024 18:08:28 +0200 Subject: [PATCH 15/26] refactor: use custom hook for hover tooltip --- lean4-infoview/src/infoview/goals.tsx | 4 +- .../src/infoview/interactiveCode.tsx | 156 +++------------ lean4-infoview/src/infoview/tooltips.tsx | 189 ++++++++++++------ 3 files changed, 156 insertions(+), 193 deletions(-) diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx index 823569614..c8ae6c6f0 100644 --- a/lean4-infoview/src/infoview/goals.tsx +++ b/lean4-infoview/src/infoview/goals.tsx @@ -80,10 +80,9 @@ interface HypNameProps { isRemoved: boolean mvarId?: string | undefined fvarId?: string | undefined - key: number } -function HypName({ name, isInserted, isRemoved, mvarId, fvarId, key }: HypNameProps) { +function HypName({ name, isInserted, isRemoved, mvarId, fvarId }: HypNameProps) { const ref = React.useRef(null) let selectionSettings: SelectionSettings @@ -112,7 +111,6 @@ function HypName({ name, isInserted, isRemoved, mvarId, fvarId, key }: HypNamePr hl.onPointerEvent(true, e)} onPointerOut={e => hl.onPointerEvent(false, e)} onPointerMove={e => hl.onPointerMove(e)} diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index d62223f43..c114feaed 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -11,10 +11,10 @@ import { } from '@leanprover/infoview-api' import { marked } from 'marked' import { Location } from 'vscode-languageserver-protocol' -import { ConfigContext, EditorContext } from './contexts' +import { EditorContext } from './contexts' import { GoalsLocation, LocationsContext, SelectionSettings, useHighlightedLocation } from './goalLocation' import { useRpcSession } from './rpcSessions' -import { TipChainContext, Tooltip, useToggleableTooltip } from './tooltips' +import { useHoverTooltip, useToggleableTooltip } from './tooltips' import { genericMemo, LogicalDomContext, @@ -158,20 +158,21 @@ const DIFF_TAG_TO_EXPLANATION: { [K in DiffTag]: string } = { function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) { const rs = useRpcSession() const ec = React.useContext(EditorContext) - const htRef = React.useRef(null) + const ref = React.useRef(null) - const [htLogicalSpanElt, htLogicalDomStorage] = useLogicalDomObserver(htRef) + const [logicalSpanElt, logicalDomStorage] = useLogicalDomObserver(ref) - const tt = useToggleableTooltip(htRef, <>{`No definition found for '${TaggedText_stripTags(fmt)}'`}) + const tt = useToggleableTooltip(ref, <>{`No definition found for '${TaggedText_stripTags(fmt)}'`}) const [setGoToDefErrorTooltipDisplayed, onClickOutsideGoToDefErrorTooltip] = [ tt.setTooltipDisplayed, tt.onClickOutside, ] + const locs = React.useContext(LocationsContext) + // We mimick the VSCode ctrl-hover and ctrl-click UI for go-to-definition const [goToLoc, setGoToLoc] = React.useState(undefined) - const locs = React.useContext(LocationsContext) let selectionSettings: SelectionSettings if (locs && locs.subexprTemplate && ct.subexprPos) { selectionSettings = { @@ -183,7 +184,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) } const hl = useHighlightedLocation({ - ref: htRef, + ref, hoverSettings: { highlightOnHover: true }, modHoverSettings: { highlightOnModHover: goToLoc !== undefined }, selectionSettings, @@ -238,108 +239,29 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) const vscodeContext = { interactiveCodeTagId } useEvent(ec.events.goToDefinition, async _ => void execGoToLoc(true), [execGoToLoc], interactiveCodeTagId) - ////////////////////////////////////////////////////////////////////////////////////////////////////////// - /* WithTooltipOnHover */ - const htConfig = React.useContext(ConfigContext) - - // We are pinned when clicked, shown when hovered over, and otherwise hidden. - type TooltipState = 'pin' | 'show' | 'hide' - const [htState, setHTState_] = React.useState('hide') - const [hoverTooltipAnchorRef, setHoverTooltipAnchorRef] = React.useState(null) - const setHTState: (state: TooltipState) => void = React.useCallback(state => { - setHTState_(state) - if (state !== 'hide') { - setHoverTooltipAnchorRef(htRef.current) + const ht = useHoverTooltip(ref, , (e, cont) => { + // On ctrl-click or ⌘-click, if location is known, go to it in the editor + if (e.ctrlKey || e.metaKey) { + setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) + void execGoToLoc(false) + return } - }, []) - const htShouldShow = htState !== 'hide' - - const htTipChainCtx = React.useContext(TipChainContext) - React.useEffect(() => { - if (htState === 'pin') htTipChainCtx.pinParent() - }, [htState, htTipChainCtx]) - const newHTTipChainCtx = React.useMemo( - () => ({ - pinParent: () => { - setHTState('pin') - htTipChainCtx.pinParent() - }, - }), - [htTipChainCtx, setHTState], - ) - - // Note: because tooltips are attached to `document.body`, they are not descendants of the - // hoverable area in the DOM tree. Thus the `contains` check fails for elements within tooltip - // contents and succeeds for elements within the hoverable. We can use this to distinguish them. - const htIsWithinHoverable = (el: EventTarget) => htRef.current && el instanceof Node && htRef.current.contains(el) - - // We use timeouts for debouncing hover events. - const htTimeout = React.useRef() - const htClearTimeout = () => { - if (htTimeout.current) { - window.clearTimeout(htTimeout.current) - htTimeout.current = undefined + if (!e.shiftKey) { + cont(e) } - } - const htShowDelay = 500 - const htHideDelay = 300 - - const htIsModifierHeld = (e: React.MouseEvent) => e.altKey || e.ctrlKey || e.shiftKey || e.metaKey - - const htOnClick = (e: React.MouseEvent) => { - htClearTimeout() - setHTState(htState === 'pin' ? 'hide' : 'pin') - e.stopPropagation() - } + }) + const onClickOutsideHoverTooltip = ht.onClickOutside - const htOnClickOutside = React.useCallback(() => { - htClearTimeout() - setHTState('hide') + const onClickOutside = React.useCallback(() => { + onClickOutsideHoverTooltip() onClickOutsideGoToDefErrorTooltip() - }, [setHTState, onClickOutsideGoToDefErrorTooltip]) - useOnClickOutside(htLogicalSpanElt, htOnClickOutside, tt.tooltipDisplayed || htShouldShow) - - const htIsPointerOverTooltip = React.useRef(false) - const htStartShowTimeout = () => { - htClearTimeout() - if (!htConfig.showTooltipOnHover) return - htTimeout.current = window.setTimeout(() => { - setHTState(htState === 'hide' ? 'show' : htState) - htTimeout.current = undefined - }, htShowDelay) - } - const htStartHideTimeout = () => { - htClearTimeout() - htTimeout.current = window.setTimeout(() => { - if (!htIsPointerOverTooltip.current) setHTState(htState === 'show' ? 'hide' : htState) - htTimeout.current = undefined - }, htHideDelay) - } - - const htOnPointerEnter = (e: React.PointerEvent) => { - htIsPointerOverTooltip.current = true - htClearTimeout() - } - - const htOnPointerLeave = (e: React.PointerEvent) => { - htIsPointerOverTooltip.current = false - htStartHideTimeout() - } - - function htGuardMouseEvent( - act: (_: React.MouseEvent) => void, - e: React.MouseEvent, - ) { - if ('_WithTooltipOnHoverSeen' in e) return - if (!htIsWithinHoverable(e.target)) return - ;(e as any)._WithTooltipOnHoverSeen = {} - act(e) - } + }, [onClickOutsideHoverTooltip, onClickOutsideGoToDefErrorTooltip]) + useOnClickOutside(logicalSpanElt, onClickOutside, tt.tooltipDisplayed || ht.state !== 'hide') return ( - + ) if (stopClick) { return } - htGuardMouseEvent(e => { - // On ctrl-click or ⌘-click, if location is known, go to it in the editor - if (e.ctrlKey || e.metaKey) { - setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) - void execGoToLoc(false) - } else if (!e.shiftKey) htOnClick(e) - }, e) + ht.onClick(e) tt.onClick() }} onPointerDown={e => { hl.onPointerDown(e) - // We have special handling for some modifier+click events, so prevent default browser - // events from interfering when a modifier is held. - if (htIsModifierHeld(e)) e.preventDefault() + ht.onPointerDown(e) }} onPointerOver={e => { hl.onPointerEvent(true, e) - if (!htIsModifierHeld(e)) { - htGuardMouseEvent(_ => htStartShowTimeout(), e) - } + ht.onPointerOver(e) }} onPointerOut={e => { hl.onPointerEvent(false, e) - htGuardMouseEvent(_ => htStartHideTimeout(), e) + ht.onPointerOut(e) }} onPointerMove={e => hl.onPointerMove(e)} onKeyDown={e => hl.onKeyDown(e)} @@ -391,17 +303,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) }} > {tt.tooltip} - {htShouldShow && ( - - - - - - )} + {ht.tooltip} diff --git a/lean4-infoview/src/infoview/tooltips.tsx b/lean4-infoview/src/infoview/tooltips.tsx index 2f5ea5448..35f3c4aea 100644 --- a/lean4-infoview/src/infoview/tooltips.tsx +++ b/lean4-infoview/src/infoview/tooltips.tsx @@ -130,41 +130,59 @@ export interface TipChainContext { export const TipChainContext = React.createContext({ pinParent: () => {} }) -export type WithTooltipOnHoverProps = Omit, 'onClick'> & { - tooltipChildren: React.ReactNode - onClick?: (event: React.MouseEvent, next: React.MouseEventHandler) => void -} +// We are pinned when clicked, shown when hovered over, and otherwise hidden. +export type TooltipState = 'pin' | 'show' | 'hide' -export function WithTooltipOnHover(props_: WithTooltipOnHoverProps) { - const { tooltipChildren, onClick: onClickProp, ...props } = props_ - const [ref, setRef] = React.useState(null) +export interface HoverTooltip { + state: TooltipState + onClick: (e: React.MouseEvent) => void + onClickOutside: () => void + onPointerDown: (e: React.PointerEvent) => void + onPointerOver: (e: React.PointerEvent) => void + onPointerOut: (e: React.PointerEvent) => void + tooltip: JSX.Element +} +export function useHoverTooltip( + ref: React.RefObject, + tooltipChildren: React.ReactNode, + guardedOnClick?: ( + e: React.MouseEvent, + cont: (e: React.MouseEvent) => void, + ) => void, +): HoverTooltip { const config = React.useContext(ConfigContext) - // We are pinned when clicked, shown when hovered over, and otherwise hidden. - type TooltipState = 'pin' | 'show' | 'hide' - const [state, setState] = React.useState('hide') - const shouldShow = state !== 'hide' + const [state, setState_] = React.useState('hide') + const [anchor, setAnchor] = React.useState(null) + const setState: (state: TooltipState) => void = React.useCallback( + state => { + setState_(state) + if (state !== 'hide') { + setAnchor(ref.current) + } + }, + [ref], + ) const tipChainCtx = React.useContext(TipChainContext) React.useEffect(() => { if (state === 'pin') tipChainCtx.pinParent() }, [state, tipChainCtx]) - const newTipChainCtx = React.useMemo( + const newHTTipChainCtx = React.useMemo( () => ({ pinParent: () => { setState('pin') tipChainCtx.pinParent() }, }), - [tipChainCtx], + [tipChainCtx, setState], ) // Note: because tooltips are attached to `document.body`, they are not descendants of the // hoverable area in the DOM tree. Thus the `contains` check fails for elements within tooltip // contents and succeeds for elements within the hoverable. We can use this to distinguish them. - const isWithinHoverable = (el: EventTarget) => ref && el instanceof Node && ref.contains(el) - const [logicalSpanElt, logicalDomStorage] = useLogicalDomObserver({ current: ref }) + const isWithinHoverable = (el: EventTarget) => ref.current && el instanceof Node && ref.current.contains(el) // We use timeouts for debouncing hover events. const timeout = React.useRef() @@ -174,36 +192,25 @@ export function WithTooltipOnHover(props_: WithTooltipOnHoverProps) { timeout.current = undefined } } + const showDelay = 500 const hideDelay = 300 - const isModifierHeld = (e: React.MouseEvent) => e.altKey || e.ctrlKey || e.shiftKey || e.metaKey - - const onClick = (e: React.MouseEvent) => { - clearTimeout() - setState(state => (state === 'pin' ? 'hide' : 'pin')) - e.stopPropagation() - } - - const onClickOutside = React.useCallback(() => { - clearTimeout() - setState('hide') - }, []) - useOnClickOutside(logicalSpanElt, onClickOutside) - - const isPointerOverTooltip = React.useRef(false) const startShowTimeout = () => { clearTimeout() if (!config.showTooltipOnHover) return timeout.current = window.setTimeout(() => { - setState(state => (state === 'hide' ? 'show' : state)) + setState(state === 'hide' ? 'show' : state) timeout.current = undefined }, showDelay) } + + const isPointerOverTooltip = React.useRef(false) + const startHideTimeout = () => { clearTimeout() timeout.current = window.setTimeout(() => { - if (!isPointerOverTooltip.current) setState(state => (state === 'show' ? 'hide' : state)) + if (!isPointerOverTooltip.current) setState(state === 'show' ? 'hide' : state) timeout.current = undefined }, hideDelay) } @@ -218,50 +225,106 @@ export function WithTooltipOnHover(props_: WithTooltipOnHoverProps) { startHideTimeout() } - function guardMouseEvent( + const guardMouseEvent = ( act: (_: React.MouseEvent) => void, e: React.MouseEvent, - ) { + ) => { if ('_WithTooltipOnHoverSeen' in e) return if (!isWithinHoverable(e.target)) return ;(e as any)._WithTooltipOnHoverSeen = {} act(e) } + const pinClick = (e: React.MouseEvent) => { + clearTimeout() + setState(state === 'pin' ? 'hide' : 'pin') + e.stopPropagation() + } + + const onClick = (e: React.MouseEvent) => { + guardMouseEvent(e => { + if (!guardedOnClick) { + pinClick(e) + return + } + guardedOnClick(e, e => pinClick(e)) + }, e) + } + + const onClickOutside = () => { + clearTimeout() + setState('hide') + } + + const isModifierHeld = (e: React.MouseEvent) => e.altKey || e.ctrlKey || e.shiftKey || e.metaKey + + const onPointerDown = (e: React.PointerEvent) => { + // We have special handling for some modifier+click events, so prevent default browser + // events from interfering when a modifier is held. + if (isModifierHeld(e)) { + e.preventDefault() + } + } + + const onPointerOver = (e: React.PointerEvent) => { + if (!isModifierHeld(e)) { + guardMouseEvent(_ => startShowTimeout(), e) + } + } + + const onPointerOut = (e: React.PointerEvent) => { + guardMouseEvent(_ => startHideTimeout(), e) + } + + const tooltip = ( + <> + {state !== 'hide' && ( + + + {tooltipChildren} + + + )} + + ) + + return { + state, + onClick, + onClickOutside, + onPointerDown, + onPointerOver, + onPointerOut, + tooltip, + } +} + +export type WithTooltipOnHoverProps = React.HTMLProps & { + tooltipChildren: React.ReactNode +} + +export function WithTooltipOnHover(props_: WithTooltipOnHoverProps) { + const { tooltipChildren, ...props } = props_ + + const ref = React.useRef(null) + + const [logicalSpanElt, logicalDomStorage] = useLogicalDomObserver(ref) + + const ht = useHoverTooltip(ref, tooltipChildren) + + useOnClickOutside(logicalSpanElt, ht.onClickOutside, ht.state !== 'hide') + return ( { - guardMouseEvent(e => { - if (onClickProp !== undefined) onClickProp(e, onClick) - else onClick(e) - }, e) - }} - onPointerDown={e => { - // We have special handling for some modifier+click events, so prevent default browser - // events from interfering when a modifier is held. - if (isModifierHeld(e)) e.preventDefault() - }} - onPointerOver={e => { - if (!isModifierHeld(e)) { - guardMouseEvent(_ => startShowTimeout(), e) - } - if (props.onPointerOver !== undefined) props.onPointerOver(e) - }} - onPointerOut={e => { - guardMouseEvent(_ => startHideTimeout(), e) - if (props.onPointerOut !== undefined) props.onPointerOut(e) - }} + ref={ref} + onClick={e => ht.onClick(e)} + onPointerDown={e => ht.onPointerDown(e)} + onPointerOver={e => ht.onPointerOver(e)} + onPointerOut={e => ht.onPointerOut(e)} > - {shouldShow && ( - - - {tooltipChildren} - - - )} + {ht.tooltip} {props.children} From cdde4a9d42c3303fea9c6233f24bfde51edae596 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 10 Jul 2024 09:45:52 +0200 Subject: [PATCH 16/26] refactor: remove devtools script --- vscode-lean4/src/infoview.ts | 1 - 1 file changed, 1 deletion(-) diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index 6f4986ccf..80dd41862 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -881,7 +881,6 @@ export class InfoProvider implements Disposable { Infoview -
From f4201e91693a4d0ae8d27475d4b24598a319b08d Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 10 Jul 2024 10:47:04 +0200 Subject: [PATCH 17/26] refactor: style and doc --- lean4-infoview/src/infoview/goalLocation.tsx | 32 +++++++++++++++---- .../src/infoview/interactiveCode.tsx | 2 ++ lean4-infoview/src/infoview/tooltips.tsx | 14 ++++++++ lean4-infoview/src/infoview/util.ts | 11 ++++--- 4 files changed, 48 insertions(+), 11 deletions(-) diff --git a/lean4-infoview/src/infoview/goalLocation.tsx b/lean4-infoview/src/infoview/goalLocation.tsx index 18ccdf4c2..8f7807c17 100644 --- a/lean4-infoview/src/infoview/goalLocation.tsx +++ b/lean4-infoview/src/infoview/goalLocation.tsx @@ -81,8 +81,17 @@ export type ModHoverSettings = { highlightOnModHover: true } | { highlightOnModH export type SelectionSettings = { highlightOnSelection: true; loc: GoalsLocation } | { highlightOnSelection: false } export interface LocationHighlightSettings { ref: React.RefObject + /** + * Whether the span should be highlighted on hover. + */ hoverSettings: HoverSettings + /** + * Whether the span should be highlighted on hover while holding `Ctrl` / `Meta`. + */ modHoverSettings: ModHoverSettings + /** + * Whether the span should be highlighted when selected, and the current {@link GoalsLocation} that is selected. + */ selectionSettings: SelectionSettings } export interface HighlightedLocation { @@ -98,7 +107,7 @@ export interface HighlightedLocation { } /** - * Logic for a `` with a corresponding {@link GoalsLocation} which can be (un)selected using shift-click. + * Logic for a `` with a corresponding {@link GoalsLocation} that can be (un)selected using shift-click. */ export function useHighlightedLocation(settings: LocationHighlightSettings): HighlightedLocation { const { ref, hoverSettings, modHoverSettings, selectionSettings } = settings @@ -124,17 +133,26 @@ export function useHighlightedLocation(settings: LocationHighlightSettings): Hig // tree and not just a logical React child (see useLogicalDom and // https://reactjs.org/docs/portals.html#event-bubbling-through-portals). if (ref.current && e.target instanceof Node && ref.current.contains(e.target)) { - if ('_DetectHoverSpanSeen' in e) return + if ('_DetectHoverSpanSeen' in e) { + return + } ;(e as any)._DetectHoverSpanSeen = {} - if (!b) setHoverState('off') - else if (e.ctrlKey || e.metaKey) setHoverState('ctrlOver') - else setHoverState('over') + if (!b) { + setHoverState('off') + } else if (e.ctrlKey || e.metaKey) { + setHoverState('ctrlOver') + } else { + setHoverState('over') + } } } const onPointerMove = (e: React.PointerEvent) => { - if (e.ctrlKey || e.metaKey) setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) - else setHoverState(st => (st === 'ctrlOver' ? 'over' : st)) + if (e.ctrlKey || e.metaKey) { + setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) + } else { + setHoverState(st => (st === 'ctrlOver' ? 'over' : st)) + } } const onKeyDown = (e: React.KeyboardEvent) => { diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index c114feaed..12fe21313 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -256,6 +256,8 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) onClickOutsideHoverTooltip() onClickOutsideGoToDefErrorTooltip() }, [onClickOutsideHoverTooltip, onClickOutsideGoToDefErrorTooltip]) + // The condition ensures that we only add the handler when a tooltip is displayed. + // These handlers can be expensive, so adding them lazily drastically improves performance. useOnClickOutside(logicalSpanElt, onClickOutside, tt.tooltipDisplayed || ht.state !== 'hide') return ( diff --git a/lean4-infoview/src/infoview/tooltips.tsx b/lean4-infoview/src/infoview/tooltips.tsx index 35f3c4aea..d4acf1ff2 100644 --- a/lean4-infoview/src/infoview/tooltips.tsx +++ b/lean4-infoview/src/infoview/tooltips.tsx @@ -72,6 +72,9 @@ export interface ToggleableTooltip { onClickOutside: () => void } +/** + * Provides handlers to show a tooltip when a state variable is changed. Hides the tooltip when clicking on it our outside of it. + */ export function useToggleableTooltip( ref: React.RefObject, tooltipChildren: React.ReactNode, @@ -81,6 +84,8 @@ export function useToggleableTooltip( const setTooltipDisplayed = (tooltipDisplayed: boolean) => { setTooltipDisplayed_(tooltipDisplayed) if (tooltipDisplayed) { + // Setting the tooltip anchor lazily only when the tooltip is displayed avoids accidental + // re-renders induced by setting this state variable during the initial render of a component. setAnchor(ref.current) } } @@ -143,6 +148,12 @@ export interface HoverTooltip { tooltip: JSX.Element } +/** Provides handlers to show a tooltip when the children of a component are hovered over or clicked. + * + * A `guardedOnClick` middleware can optionally be given in order to control what happens when the + * hoverable area is clicked. The middleware can invoke `cont` to execute the default action, + * which is to pin the tooltip open. + */ export function useHoverTooltip( ref: React.RefObject, tooltipChildren: React.ReactNode, @@ -303,6 +314,9 @@ export type WithTooltipOnHoverProps = React.HTMLProps & { tooltipChildren: React.ReactNode } +/** + * Span that uses the logic of {@link useHoverTooltip}. + */ export function WithTooltipOnHover(props_: WithTooltipOnHoverProps) { const { tooltipChildren, ...props } = props_ diff --git a/lean4-infoview/src/infoview/util.ts b/lean4-infoview/src/infoview/util.ts index fecffc83a..ca281479b 100644 --- a/lean4-infoview/src/infoview/util.ts +++ b/lean4-infoview/src/infoview/util.ts @@ -287,14 +287,17 @@ export function useLogicalDomObserver(elt: React.RefObject): [Logic /** * An effect which calls `onClickOutside` whenever an element not logically descending from `ld` * (see {@link useLogicalDomObserver}) is clicked. Note that `onClickOutside` is not called on clicks - * on the scrollbar since these should usually not impact the app's state. */ + * on the scrollbar since these should usually not impact the app's state. + * `isActive` controls whether the `onClickOutside` handler is active. This can be useful for performance, + * since having lots of `onClickOutside` handlers when they are not needed can be expensive. + */ export function useOnClickOutside( ld: LogicalDomElement, onClickOutside: (_: PointerEvent) => void, - trigger: boolean = true, + isActive: boolean = true, ) { React.useEffect(() => { - if (!trigger) { + if (!isActive) { return } const onClickAnywhere = (e: PointerEvent) => { @@ -308,7 +311,7 @@ export function useOnClickOutside( document.addEventListener('pointerdown', onClickAnywhere) return () => document.removeEventListener('pointerdown', onClickAnywhere) - }, [ld, onClickOutside, trigger]) + }, [ld, onClickOutside, isActive]) } /** Sends an exception object to a throwable error. From d963a648dd6656d7c97e4bd93dae3183f5117d83 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 10 Jul 2024 11:03:31 +0200 Subject: [PATCH 18/26] chore: bump infoview minor version --- lean4-infoview/package.json | 2 +- package-lock.json | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lean4-infoview/package.json b/lean4-infoview/package.json index 2eea7c74e..56f4871df 100644 --- a/lean4-infoview/package.json +++ b/lean4-infoview/package.json @@ -1,6 +1,6 @@ { "name": "@leanprover/infoview", - "version": "0.7.2", + "version": "0.7.3", "description": "An interactive display for the Lean 4 theorem prover.", "scripts": { "watch": "rollup --config --environment NODE_ENV:development --watch", diff --git a/package-lock.json b/package-lock.json index 71e4f771e..5a787b087 100644 --- a/package-lock.json +++ b/package-lock.json @@ -28,7 +28,7 @@ }, "lean4-infoview": { "name": "@leanprover/infoview", - "version": "0.7.1", + "version": "0.7.3", "license": "Apache-2.0", "dependencies": { "@leanprover/infoview-api": "~0.4.0", @@ -14109,7 +14109,7 @@ }, "vscode-lean4": { "name": "lean4", - "version": "0.0.163", + "version": "0.0.171", "license": "Apache-2.0", "dependencies": { "@leanprover/infoview": "~0.7.0", From c8774867db0b9dd5d3d88fb9bff45a3cea085f0f Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 10 Jul 2024 14:23:00 +0200 Subject: [PATCH 19/26] test: adjust test for changes --- vscode-lean4/test/suite/info/info.test.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/vscode-lean4/test/suite/info/info.test.ts b/vscode-lean4/test/suite/info/info.test.ts index 45e2120c0..17f9027a2 100644 --- a/vscode-lean4/test/suite/info/info.test.ts +++ b/vscode-lean4/test/suite/info/info.test.ts @@ -190,7 +190,7 @@ suite('InfoView Test Suite', () => { logger.log('Opening tooltip in tooltip') await info.runTestScript(` - Array.from(document.querySelectorAll('.tooltip-content [data-has-tooltip-on-hover] *')) + Array.from(document.querySelectorAll('.tooltip-content *[data-has-tooltip-on-hover]')) .find(el => el.innerHTML === 'Type 4') .click() `) @@ -198,7 +198,7 @@ suite('InfoView Test Suite', () => { logger.log('Opening tooltip in tooltip in tooltip') await info.runTestScript(` - Array.from(document.querySelectorAll('.tooltip-content [data-has-tooltip-on-hover] *')) + Array.from(document.querySelectorAll('.tooltip-content *[data-has-tooltip-on-hover]')) .find(el => el.innerHTML === 'Type 5') .click() `) From 0889d2776fa71fbc3c3ce62ad12454653755b4f8 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 18 Jul 2024 15:31:48 +0200 Subject: [PATCH 20/26] refactor: do not export TipChainContext --- lean4-infoview/src/infoview/tooltips.tsx | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lean4-infoview/src/infoview/tooltips.tsx b/lean4-infoview/src/infoview/tooltips.tsx index d4acf1ff2..ce356e82a 100644 --- a/lean4-infoview/src/infoview/tooltips.tsx +++ b/lean4-infoview/src/infoview/tooltips.tsx @@ -129,11 +129,11 @@ export function useToggleableTooltip( export type HoverState = 'off' | 'over' | 'ctrlOver' /** Pinning a child tooltip has to also pin all ancestors. This context supports that. */ -export interface TipChainContext { +interface TipChainContext { pinParent(): void } -export const TipChainContext = React.createContext({ pinParent: () => {} }) +const TipChainContext = React.createContext({ pinParent: () => {} }) // We are pinned when clicked, shown when hovered over, and otherwise hidden. export type TooltipState = 'pin' | 'show' | 'hide' From 902a8f8944753d42d4b8b29eb0177b6a1799b816 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 18 Jul 2024 16:00:42 +0200 Subject: [PATCH 21/26] doc: adjust comment per review --- lean4-infoview/src/infoview/tooltips.tsx | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lean4-infoview/src/infoview/tooltips.tsx b/lean4-infoview/src/infoview/tooltips.tsx index ce356e82a..5509544d1 100644 --- a/lean4-infoview/src/infoview/tooltips.tsx +++ b/lean4-infoview/src/infoview/tooltips.tsx @@ -73,7 +73,8 @@ export interface ToggleableTooltip { } /** - * Provides handlers to show a tooltip when a state variable is changed. Hides the tooltip when clicking on it our outside of it. + * Provides handlers to show a tooltip when a state variable is changed. + * The tooltip is hidden when a click is made anywhere (on or outside the tooltip). */ export function useToggleableTooltip( ref: React.RefObject, From 433fa8928f93fd992837393b6b0bcdcde9207bd7 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 18 Jul 2024 17:13:25 +0200 Subject: [PATCH 22/26] refactor: highlighted location comments --- lean4-infoview/src/infoview/goalLocation.tsx | 107 +++--------------- lean4-infoview/src/infoview/goals.tsx | 42 +++---- .../src/infoview/hoverHighlight.tsx | 98 ++++++++++++++++ lean4-infoview/src/infoview/index.css | 8 +- .../src/infoview/interactiveCode.tsx | 47 ++++---- 5 files changed, 164 insertions(+), 138 deletions(-) create mode 100644 lean4-infoview/src/infoview/hoverHighlight.tsx diff --git a/lean4-infoview/src/infoview/goalLocation.tsx b/lean4-infoview/src/infoview/goalLocation.tsx index 8f7807c17..62b3827ab 100644 --- a/lean4-infoview/src/infoview/goalLocation.tsx +++ b/lean4-infoview/src/infoview/goalLocation.tsx @@ -5,7 +5,6 @@ Authors: E.W.Ayers, Wojciech Nawrocki */ import { FVarId, MVarId, SubexprPos } from '@leanprover/infoview-api' import * as React from 'react' -import { HoverState } from './tooltips' /** * A location within a goal. It is either: @@ -76,102 +75,34 @@ export interface Locations { export const LocationsContext = React.createContext(undefined) -export type HoverSettings = { highlightOnHover: true } | { highlightOnHover: false } -export type ModHoverSettings = { highlightOnModHover: true } | { highlightOnModHover: false } -export type SelectionSettings = { highlightOnSelection: true; loc: GoalsLocation } | { highlightOnSelection: false } -export interface LocationHighlightSettings { - ref: React.RefObject - /** - * Whether the span should be highlighted on hover. - */ - hoverSettings: HoverSettings - /** - * Whether the span should be highlighted on hover while holding `Ctrl` / `Meta`. - */ - modHoverSettings: ModHoverSettings - /** - * Whether the span should be highlighted when selected, and the current {@link GoalsLocation} that is selected. - */ - selectionSettings: SelectionSettings -} -export interface HighlightedLocation { - hoverState: HoverState - setHoverState: React.Dispatch> +export type SelectableLocationSettings = + | { + isSelectable: true + /** The {@link GoalsLocation} that can be selected by interacting with the span. */ + loc: GoalsLocation + } + | { isSelectable: false } + +export interface SelectableLocation { className: string - onPointerEvent: (b: boolean, e: React.PointerEvent) => void - onPointerMove: (e: React.PointerEvent) => void - onKeyDown: (e: React.KeyboardEvent) => void - onKeyUp: (e: React.KeyboardEvent) => void + /** Returns whether propagation of the click event within the same handler should be stopped. */ onClick: (e: React.MouseEvent) => boolean onPointerDown: (e: React.PointerEvent) => void } -/** - * Logic for a `` with a corresponding {@link GoalsLocation} that can be (un)selected using shift-click. - */ -export function useHighlightedLocation(settings: LocationHighlightSettings): HighlightedLocation { - const { ref, hoverSettings, modHoverSettings, selectionSettings } = settings - - const [hoverState, setHoverState] = React.useState('off') - +/** Logic for a span that can be selected using Shift-click and is highlighted when selected. */ +export function useSelectableLocation(settings: SelectableLocationSettings): SelectableLocation { const locs = React.useContext(LocationsContext) let className: string = '' - if (hoverSettings.highlightOnHover && hoverState !== 'off') { - className += 'highlight ' - } else if (selectionSettings.highlightOnSelection && locs && locs.isSelected(selectionSettings.loc)) { + if (settings.isSelectable && locs && locs.isSelected(settings.loc)) { className += 'highlight-selected ' } - if (modHoverSettings.highlightOnModHover && hoverState === 'ctrlOver') { - className += 'underline ' - } - - const onPointerEvent = (b: boolean, e: React.PointerEvent) => { - // It's more composable to let pointer events bubble up rather than to call `stopPropagation`, - // but we only want to handle hovers in the innermost component. So we record that the - // event was handled with a property. - // The `contains` check ensures that the node hovered over is a child in the DOM - // tree and not just a logical React child (see useLogicalDom and - // https://reactjs.org/docs/portals.html#event-bubbling-through-portals). - if (ref.current && e.target instanceof Node && ref.current.contains(e.target)) { - if ('_DetectHoverSpanSeen' in e) { - return - } - ;(e as any)._DetectHoverSpanSeen = {} - if (!b) { - setHoverState('off') - } else if (e.ctrlKey || e.metaKey) { - setHoverState('ctrlOver') - } else { - setHoverState('over') - } - } - } - - const onPointerMove = (e: React.PointerEvent) => { - if (e.ctrlKey || e.metaKey) { - setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) - } else { - setHoverState(st => (st === 'ctrlOver' ? 'over' : st)) - } - } - - const onKeyDown = (e: React.KeyboardEvent) => { - if (e.key === 'Control' || e.key === 'Meta') { - setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) - } - } - - const onKeyUp = (e: React.KeyboardEvent) => { - if (e.key === 'Control' || e.key === 'Meta') { - setHoverState(st => (st === 'ctrlOver' ? 'over' : st)) - } - } const onClick = (e: React.MouseEvent) => { // On shift-click, if we are in a context where selecting subexpressions makes sense, // (un)select the current subexpression. - if (selectionSettings.highlightOnSelection && locs && e.shiftKey) { - locs.setSelected(selectionSettings.loc, on => !on) + if (settings.isSelectable && locs && e.shiftKey) { + locs.setSelected(settings.loc, on => !on) e.stopPropagation() return true } @@ -181,19 +112,13 @@ export function useHighlightedLocation(settings: LocationHighlightSettings): Hig const onPointerDown = (e: React.PointerEvent) => { // We have special handling for shift+click events, so prevent default browser // events from interfering when shift is held. - if (selectionSettings.highlightOnSelection && locs && e.shiftKey) { + if (settings.isSelectable && locs && e.shiftKey) { e.preventDefault() } } return { - hoverState, - setHoverState, className, - onPointerEvent, - onPointerMove, - onKeyDown, - onKeyUp, onClick, onPointerDown, } diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx index c8ae6c6f0..065ab8a03 100644 --- a/lean4-infoview/src/infoview/goals.tsx +++ b/lean4-infoview/src/infoview/goals.tsx @@ -10,7 +10,8 @@ import { import * as React from 'react' import { Details } from './collapsing' import { ConfigContext, EditorContext } from './contexts' -import { Locations, LocationsContext, SelectionSettings, useHighlightedLocation } from './goalLocation' +import { Locations, LocationsContext, SelectableLocationSettings, useSelectableLocation } from './goalLocation' +import { useHoverHighlight } from './hoverHighlight' import { InteractiveCode } from './interactiveCode' import { WithTooltipOnHover } from './tooltips' import { useEvent } from './util' @@ -85,39 +86,40 @@ interface HypNameProps { function HypName({ name, isInserted, isRemoved, mvarId, fvarId }: HypNameProps) { const ref = React.useRef(null) - let selectionSettings: SelectionSettings - if (mvarId !== undefined && fvarId !== undefined) { - selectionSettings = { highlightOnSelection: true, loc: { mvarId, loc: { hyp: fvarId } } } - } else { - selectionSettings = { highlightOnSelection: false } - } - const locs = React.useContext(LocationsContext) - const hl = useHighlightedLocation({ + const hhl = useHoverHighlight({ ref, - hoverSettings: { highlightOnHover: locs !== undefined && mvarId !== undefined && fvarId !== undefined }, - modHoverSettings: { highlightOnModHover: false }, - selectionSettings, + highlightOnHover: locs !== undefined && mvarId !== undefined && fvarId !== undefined, + underlineOnModHover: false, }) + let selectableLocationSettings: SelectableLocationSettings + if (mvarId !== undefined && fvarId !== undefined) { + selectableLocationSettings = { isSelectable: true, loc: { mvarId, loc: { hyp: fvarId } } } + } else { + selectableLocationSettings = { isSelectable: false } + } + const sl = useSelectableLocation(selectableLocationSettings) + const namecls: string = (isInserted ? 'inserted-text ' : '') + (isRemoved ? 'removed-text ' : '') + (isInaccessibleName(name) ? 'goal-inaccessible ' : '') + - hl.className + hhl.className + + sl.className return ( <> hl.onPointerEvent(true, e)} - onPointerOut={e => hl.onPointerEvent(false, e)} - onPointerMove={e => hl.onPointerMove(e)} - onKeyDown={e => hl.onKeyDown(e)} - onKeyUp={e => hl.onKeyUp(e)} - onClick={e => hl.onClick(e)} - onPointerDown={e => hl.onPointerDown(e)} + onPointerOver={e => hhl.onPointerOver(e)} + onPointerOut={e => hhl.onPointerOut(e)} + onPointerMove={e => hhl.onPointerMove(e)} + onKeyDown={e => hhl.onKeyDown(e)} + onKeyUp={e => hhl.onKeyUp(e)} + onClick={e => sl.onClick(e)} + onPointerDown={e => sl.onPointerDown(e)} > {name} diff --git a/lean4-infoview/src/infoview/hoverHighlight.tsx b/lean4-infoview/src/infoview/hoverHighlight.tsx new file mode 100644 index 000000000..791869a02 --- /dev/null +++ b/lean4-infoview/src/infoview/hoverHighlight.tsx @@ -0,0 +1,98 @@ +import React from 'react' +import { HoverState } from './tooltips' + +export interface HoverHighlightSettings { + ref: React.RefObject + /** + * Whether the span should be highlighted on hover. + */ + highlightOnHover: boolean + /** + * Whether the span should be underlined on hover while holding `Ctrl` / `Meta`. + */ + underlineOnModHover: boolean +} + +export interface HoverHighlight { + hoverState: HoverState + setHoverState: React.Dispatch> + className: string + onPointerOver: (e: React.PointerEvent) => void + onPointerOut: (e: React.PointerEvent) => void + onPointerMove: (e: React.PointerEvent) => void + onKeyDown: (e: React.KeyboardEvent) => void + onKeyUp: (e: React.KeyboardEvent) => void +} + +/** + * Logic for a span that can be highlighted when hovering over it + * and underlined when hovering over it while holding `Ctrl` / `Meta`. + */ +export function useHoverHighlight(settings: HoverHighlightSettings): HoverHighlight { + const { ref, highlightOnHover, underlineOnModHover } = settings + + const [hoverState, setHoverState] = React.useState('off') + + let className: string = '' + if (highlightOnHover && hoverState !== 'off') { + className += 'highlight ' + } + if (underlineOnModHover && hoverState === 'ctrlOver') { + className += 'underline ' + } + + const onPointerEvent = (b: boolean, e: React.PointerEvent) => { + // It's more composable to let pointer events bubble up rather than to call `stopPropagation`, + // but we only want to handle hovers in the innermost component. So we record that the + // event was handled with a property. + // The `contains` check ensures that the node hovered over is a child in the DOM + // tree and not just a logical React child (see useLogicalDom and + // https://reactjs.org/docs/portals.html#event-bubbling-through-portals). + if (ref.current && e.target instanceof Node && ref.current.contains(e.target)) { + if ('_DetectHoverSpanSeen' in e) { + return + } + ;(e as any)._DetectHoverSpanSeen = {} + if (!b) { + setHoverState('off') + } else if (e.ctrlKey || e.metaKey) { + setHoverState('ctrlOver') + } else { + setHoverState('over') + } + } + } + const onPointerOver = (e: React.PointerEvent) => onPointerEvent(true, e) + const onPointerOut = (e: React.PointerEvent) => onPointerEvent(false, e) + + const onPointerMove = (e: React.PointerEvent) => { + if (e.ctrlKey || e.metaKey) { + setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) + } else { + setHoverState(st => (st === 'ctrlOver' ? 'over' : st)) + } + } + + const onKeyDown = (e: React.KeyboardEvent) => { + if (e.key === 'Control' || e.key === 'Meta') { + setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) + } + } + + const onKeyUp = (e: React.KeyboardEvent) => { + if (e.key === 'Control' || e.key === 'Meta') { + setHoverState(st => (st === 'ctrlOver' ? 'over' : st)) + } + } + + return { + hoverState, + setHoverState, + className, + onPointerOver, + onPointerOut, + onPointerMove, + onKeyDown, + onKeyUp, + } +} diff --git a/lean4-infoview/src/infoview/index.css b/lean4-infoview/src/infoview/index.css index e16f2314b..513ecdadc 100644 --- a/lean4-infoview/src/infoview/index.css +++ b/lean4-infoview/src/infoview/index.css @@ -49,14 +49,14 @@ body { font-weight: normal; } -.highlight { - background-color: var(--vscode-editor-selectionBackground) !important; -} - .highlight-selected { background-color: var(--vscode-editorOverviewRuler-rangeHighlightForeground) !important; } +.highlight { + background-color: var(--vscode-editor-selectionBackground) !important; +} + /* Interactive traces */ .trace-line:hover { background-color: #dbeeff; diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index 12fe21313..aa0eb83e5 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -12,7 +12,8 @@ import { import { marked } from 'marked' import { Location } from 'vscode-languageserver-protocol' import { EditorContext } from './contexts' -import { GoalsLocation, LocationsContext, SelectionSettings, useHighlightedLocation } from './goalLocation' +import { GoalsLocation, LocationsContext, SelectableLocationSettings, useSelectableLocation } from './goalLocation' +import { useHoverHighlight } from './hoverHighlight' import { useRpcSession } from './rpcSessions' import { useHoverTooltip, useToggleableTooltip } from './tooltips' import { @@ -168,28 +169,28 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) tt.onClickOutside, ] - const locs = React.useContext(LocationsContext) - // We mimick the VSCode ctrl-hover and ctrl-click UI for go-to-definition const [goToLoc, setGoToLoc] = React.useState(undefined) - let selectionSettings: SelectionSettings + const hhl = useHoverHighlight({ + ref, + highlightOnHover: true, + underlineOnModHover: goToLoc !== undefined, + }) + const [hoverState, setHoverState] = [hhl.hoverState, hhl.setHoverState] + + const locs = React.useContext(LocationsContext) + + let selectableLocationSettings: SelectableLocationSettings if (locs && locs.subexprTemplate && ct.subexprPos) { - selectionSettings = { - highlightOnSelection: true, + selectableLocationSettings = { + isSelectable: true, loc: GoalsLocation.withSubexprPos(locs.subexprTemplate, ct.subexprPos), } } else { - selectionSettings = { highlightOnSelection: false } + selectableLocationSettings = { isSelectable: false } } - - const hl = useHighlightedLocation({ - ref, - hoverSettings: { highlightOnHover: true }, - modHoverSettings: { highlightOnModHover: goToLoc !== undefined }, - selectionSettings, - }) - const [hoverState, setHoverState] = [hl.hoverState, hl.setHoverState] + const sl = useSelectableLocation(selectableLocationSettings) const fetchGoToLoc = React.useCallback(async () => { if (goToLoc !== undefined) return goToLoc @@ -226,7 +227,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) [fetchGoToLoc, ec, setGoToDefErrorTooltipDisplayed], ) - let className = hl.className + let className = hhl.className + sl.className if (ct.diffStatus) { className += DIFF_TAG_TO_CLASS[ct.diffStatus] + ' ' } @@ -268,7 +269,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) data-vscode-context={JSON.stringify(vscodeContext)} data-has-tooltip-on-hover onClick={e => { - const stopClick = hl.onClick(e) + const stopClick = sl.onClick(e) if (stopClick) { return } @@ -276,20 +277,20 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) tt.onClick() }} onPointerDown={e => { - hl.onPointerDown(e) + sl.onPointerDown(e) ht.onPointerDown(e) }} onPointerOver={e => { - hl.onPointerEvent(true, e) + hhl.onPointerOver(e) ht.onPointerOver(e) }} onPointerOut={e => { - hl.onPointerEvent(false, e) + hhl.onPointerOut(e) ht.onPointerOut(e) }} - onPointerMove={e => hl.onPointerMove(e)} - onKeyDown={e => hl.onKeyDown(e)} - onKeyUp={e => hl.onKeyUp(e)} + onPointerMove={e => hhl.onPointerMove(e)} + onKeyDown={e => hhl.onKeyDown(e)} + onKeyUp={e => hhl.onKeyUp(e)} onContextMenu={e => { // Mark the event as seen so that parent handlers skip it. // We cannot use `stopPropagation` as that prevents the VSC context menu from showing up. From cea9f0bbc0f754eca9b9e73871f1644734bdbd61 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 19 Jul 2024 15:45:00 +0200 Subject: [PATCH 23/26] doc: generalize descriptions --- lean4-infoview/src/infoview/goalLocation.tsx | 7 ++++++- lean4-infoview/src/infoview/hoverHighlight.tsx | 12 ++++++++---- 2 files changed, 14 insertions(+), 5 deletions(-) diff --git a/lean4-infoview/src/infoview/goalLocation.tsx b/lean4-infoview/src/infoview/goalLocation.tsx index 62b3827ab..4c5c2bb1e 100644 --- a/lean4-infoview/src/infoview/goalLocation.tsx +++ b/lean4-infoview/src/infoview/goalLocation.tsx @@ -90,7 +90,12 @@ export interface SelectableLocation { onPointerDown: (e: React.PointerEvent) => void } -/** Logic for a span that can be selected using Shift-click and is highlighted when selected. */ +/** + * 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. + */ export function useSelectableLocation(settings: SelectableLocationSettings): SelectableLocation { const locs = React.useContext(LocationsContext) let className: string = '' diff --git a/lean4-infoview/src/infoview/hoverHighlight.tsx b/lean4-infoview/src/infoview/hoverHighlight.tsx index 791869a02..bf9b2cbd1 100644 --- a/lean4-infoview/src/infoview/hoverHighlight.tsx +++ b/lean4-infoview/src/infoview/hoverHighlight.tsx @@ -4,11 +4,11 @@ import { HoverState } from './tooltips' export interface HoverHighlightSettings { ref: React.RefObject /** - * Whether the span should be highlighted on hover. + * Whether to return the `highlight` CSS class on hover. */ highlightOnHover: boolean /** - * Whether the span should be underlined on hover while holding `Ctrl` / `Meta`. + * Whether to return the `underline` CSS class on hover while holding `Ctrl` / `Meta`. */ underlineOnModHover: boolean } @@ -25,8 +25,12 @@ export interface HoverHighlight { } /** - * Logic for a span that can be highlighted when hovering over it - * and underlined when hovering over it while holding `Ctrl` / `Meta`. + * Logic for a component that is highlighted/underlined when hovered over. + * The component is passed in `settings.ref`. + * + * The hook returns the current hover state of the component, + * a string of CSS classes containing `highlight` and/or `underline` when appropriate, + * as well as event handlers which the the caller must attach to the component. */ export function useHoverHighlight(settings: HoverHighlightSettings): HoverHighlight { const { ref, highlightOnHover, underlineOnModHover } = settings From ce95f91fbde3f2779b4a1d22dc71cbd6813c3d6e Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 19 Jul 2024 16:14:22 +0200 Subject: [PATCH 24/26] feat: memoize InteractiveTaggedText --- .../src/infoview/interactiveCode.tsx | 31 ++++++++----------- lean4-infoview/src/infoview/util.ts | 5 --- 2 files changed, 13 insertions(+), 23 deletions(-) diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index aa0eb83e5..17fcbf73f 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -16,15 +16,7 @@ import { GoalsLocation, LocationsContext, SelectableLocationSettings, useSelecta import { useHoverHighlight } from './hoverHighlight' import { useRpcSession } from './rpcSessions' import { useHoverTooltip, useToggleableTooltip } from './tooltips' -import { - genericMemo, - LogicalDomContext, - mapRpcError, - useAsync, - useEvent, - useLogicalDomObserver, - useOnClickOutside, -} from './util' +import { LogicalDomContext, mapRpcError, useAsync, useEvent, useLogicalDomObserver, useOnClickOutside } from './util' export interface InteractiveTextComponentProps { fmt: TaggedText @@ -38,11 +30,8 @@ export interface InteractiveTaggedTextProps extends InteractiveTextComponentP InnerTagUi: (_: InteractiveTagProps) => JSX.Element } -/** - * Core loop to display {@link TaggedText} objects. Invokes `InnerTagUi` on `tag` nodes in order to support - * various embedded information, for example subexpression information stored in {@link CodeWithInfos}. - * */ -export function InteractiveTaggedText({ fmt, InnerTagUi }: InteractiveTaggedTextProps) { +// See https://github.com/leanprover/vscode-lean4/pull/500#discussion_r1681001815 for why `any` is used. +const InteractiveTaggedText_ = React.memo(({ fmt, InnerTagUi }: InteractiveTaggedTextProps) => { if ('text' in fmt) return <>{fmt.text} else if ('append' in fmt) return ( @@ -54,9 +43,15 @@ export function InteractiveTaggedText({ fmt, InnerTagUi }: InteractiveTaggedT ) else if ('tag' in fmt) return else throw new Error(`malformed 'TaggedText': '${fmt}'`) -} +}) -export const MemoedInteractiveTaggedText = genericMemo(InteractiveTaggedText) +/** + * Core loop to display {@link TaggedText} objects. Invokes `InnerTagUi` on `tag` nodes in order to support + * various embedded information, for example subexpression information stored in {@link CodeWithInfos}. + */ +export function InteractiveTaggedText({ fmt, InnerTagUi }: InteractiveTaggedTextProps) { + return +} interface TypePopupContentsProps { info: SubexprInfo @@ -307,7 +302,7 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) > {tt.tooltip} {ht.tooltip} - + ) @@ -319,7 +314,7 @@ export type InteractiveCodeProps = InteractiveTextComponentProps export function InteractiveCode(props: InteractiveCodeProps) { return ( - + ) } diff --git a/lean4-infoview/src/infoview/util.ts b/lean4-infoview/src/infoview/util.ts index ca281479b..4c2d4a4b5 100644 --- a/lean4-infoview/src/infoview/util.ts +++ b/lean4-infoview/src/infoview/util.ts @@ -427,8 +427,3 @@ export function useAsyncPersistent(fn: () => Promise, deps: React.Dependen } return state } - -/** - * Memoizes a generic component in a way that does not require a type cast. - */ -export const genericMemo: (component: T) => T = React.memo From c04086e3d2a5000e81b45f1cfa389e0b41b962f1 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 19 Jul 2024 17:17:43 +0200 Subject: [PATCH 25/26] fix: accurately detect `Ctrl` inputs --- lean4-infoview/src/infoview/goals.tsx | 2 -- .../src/infoview/hoverHighlight.tsx | 32 +++++++++++++------ .../src/infoview/interactiveCode.tsx | 2 -- 3 files changed, 23 insertions(+), 13 deletions(-) diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx index 065ab8a03..e0405061e 100644 --- a/lean4-infoview/src/infoview/goals.tsx +++ b/lean4-infoview/src/infoview/goals.tsx @@ -116,8 +116,6 @@ function HypName({ name, isInserted, isRemoved, mvarId, fvarId }: HypNameProps) onPointerOver={e => hhl.onPointerOver(e)} onPointerOut={e => hhl.onPointerOut(e)} onPointerMove={e => hhl.onPointerMove(e)} - onKeyDown={e => hhl.onKeyDown(e)} - onKeyUp={e => hhl.onKeyUp(e)} onClick={e => sl.onClick(e)} onPointerDown={e => sl.onPointerDown(e)} > diff --git a/lean4-infoview/src/infoview/hoverHighlight.tsx b/lean4-infoview/src/infoview/hoverHighlight.tsx index 791869a02..d716d2128 100644 --- a/lean4-infoview/src/infoview/hoverHighlight.tsx +++ b/lean4-infoview/src/infoview/hoverHighlight.tsx @@ -20,8 +20,6 @@ export interface HoverHighlight { onPointerOver: (e: React.PointerEvent) => void onPointerOut: (e: React.PointerEvent) => void onPointerMove: (e: React.PointerEvent) => void - onKeyDown: (e: React.KeyboardEvent) => void - onKeyUp: (e: React.KeyboardEvent) => void } /** @@ -32,9 +30,10 @@ export function useHoverHighlight(settings: HoverHighlightSettings): HoverHighli const { ref, highlightOnHover, underlineOnModHover } = settings const [hoverState, setHoverState] = React.useState('off') + const isHoveredOver = hoverState !== 'off' let className: string = '' - if (highlightOnHover && hoverState !== 'off') { + if (highlightOnHover && isHoveredOver) { className += 'highlight ' } if (underlineOnModHover && hoverState === 'ctrlOver') { @@ -73,17 +72,34 @@ export function useHoverHighlight(settings: HoverHighlightSettings): HoverHighli } } - const onKeyDown = (e: React.KeyboardEvent) => { + const onKeyDown = React.useCallback((e: KeyboardEvent) => { if (e.key === 'Control' || e.key === 'Meta') { setHoverState(st => (st === 'over' ? 'ctrlOver' : st)) } - } + }, []) - const onKeyUp = (e: React.KeyboardEvent) => { + const onKeyUp = React.useCallback((e: KeyboardEvent) => { if (e.key === 'Control' || e.key === 'Meta') { setHoverState(st => (st === 'ctrlOver' ? 'over' : st)) } - } + }, []) + + React.useEffect(() => { + if (!isHoveredOver) { + // Avoid adding lots of expensive global event handlers for spans that are not being + // hovered over + return + } + + // These event handlers do not fire when the InfoView is not focused. + document.addEventListener('keydown', onKeyDown) + document.addEventListener('keyup', onKeyUp) + + return () => { + document.removeEventListener('keydown', onKeyDown) + document.removeEventListener('keyup', onKeyUp) + } + }, [onKeyDown, onKeyUp, isHoveredOver]) return { hoverState, @@ -92,7 +108,5 @@ export function useHoverHighlight(settings: HoverHighlightSettings): HoverHighli onPointerOver, onPointerOut, onPointerMove, - onKeyDown, - onKeyUp, } } diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index aa0eb83e5..14e533bb1 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -289,8 +289,6 @@ function InteractiveCodeTag({ tag: ct, fmt }: InteractiveTagProps) ht.onPointerOut(e) }} onPointerMove={e => hhl.onPointerMove(e)} - onKeyDown={e => hhl.onKeyDown(e)} - onKeyUp={e => hhl.onKeyUp(e)} onContextMenu={e => { // Mark the event as seen so that parent handlers skip it. // We cannot use `stopPropagation` as that prevents the VSC context menu from showing up. From 0dda8257359d2f4c02c03868f454f792700659d8 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 19 Jul 2024 18:04:38 +0200 Subject: [PATCH 26/26] fix: performance regression --- lean4-infoview/src/infoview/interactiveCode.tsx | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index 6ddfb069b..48008434e 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -31,19 +31,21 @@ export interface InteractiveTaggedTextProps extends InteractiveTextComponentP } // See https://github.com/leanprover/vscode-lean4/pull/500#discussion_r1681001815 for why `any` is used. -const InteractiveTaggedText_ = React.memo(({ fmt, InnerTagUi }: InteractiveTaggedTextProps) => { +function InteractiveTaggedText__({ fmt, InnerTagUi }: InteractiveTaggedTextProps) { if ('text' in fmt) return <>{fmt.text} else if ('append' in fmt) return ( <> {fmt.append.map((a, i) => ( - + ))} ) else if ('tag' in fmt) return else throw new Error(`malformed 'TaggedText': '${fmt}'`) -}) +} + +const InteractiveTaggedText_ = React.memo(InteractiveTaggedText__) /** * Core loop to display {@link TaggedText} objects. Invokes `InnerTagUi` on `tag` nodes in order to support