fix: filter menu button collapsing goal state (#511)

Closes #505. --------- Co-authored-by: Wojciech Nawrocki <[email protected]>
leanprover · Aug 4, 2024 · 93095f9 · 93095f9
1 parent e153595
commit 93095f9
Show file tree

Hide file tree

Showing 7 changed files with 26 additions and 15 deletions.
diff --git a/lean4-infoview/src/infoview/collapsing.tsx b/lean4-infoview/src/infoview/collapsing.tsx
@@ -32,18 +32,23 @@ interface DetailsProps {
     setOpenRef?: (_: React.Dispatch<React.SetStateAction<boolean>>) => void
 }
 
-/** Like `<details>` but can be programatically revealed using `setOpenRef`. */
+/** Like `<details>` but can be programatically revealed using `setOpenRef`.
+ * The first child is placed inside the `<summary>` node. */
 export function Details({ initiallyOpen, children: [summary, ...children], setOpenRef }: DetailsProps): JSX.Element {
     const [isOpen, setOpen] = React.useState<boolean>(initiallyOpen === undefined ? false : initiallyOpen)
-    const setupEventListener = React.useCallback((node: HTMLDetailsElement | null) => {
-        if (node !== undefined && node !== null) {
-            node.addEventListener('toggle', () => setOpen(node.open))
-        }
-    }, [])
     if (setOpenRef) setOpenRef(setOpen)
     return (
-        <details ref={setupEventListener} open={isOpen}>
-            {summary}
+        <details open={isOpen}>
+            <summary
+                className="mv2 pointer "
+                onClick={e => {
+                    if (!e.defaultPrevented) setOpen(!isOpen)
+                    // See https://github.com/facebook/react/issues/15486#issuecomment-873516817
+                    e.preventDefault()
+                }}
+            >
+                {summary}
+            </summary>
             {isOpen && children}
         </details>
     )

diff --git a/lean4-infoview/src/infoview/goalLocation.tsx b/lean4-infoview/src/infoview/goalLocation.tsx
@@ -109,6 +109,7 @@ export function useSelectableLocation(settings: SelectableLocationSettings): Sel
         if (settings.isSelectable && locs && e.shiftKey) {
             locs.setSelected(settings.loc, on => !on)
             e.stopPropagation()
+            e.preventDefault()
             return true
         }
         return false

diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx
@@ -403,7 +403,7 @@ export const FilteredGoals = React.memo(
         return (
             <div style={{ display: goals !== undefined ? 'block' : 'none' }}>
                 <Details setOpenRef={r => (setOpenRef.current = r)} initiallyOpen={initiallyOpen}>
-                    <summary className="mv2 pointer">
+                    <>
                         {headerChildren}
                         <span
                             className="fr"
@@ -415,7 +415,7 @@ export const FilteredGoals = React.memo(
                             {sortButton}
                             {filterButton}
                         </span>
-                    </summary>
+                    </>
                     <div className="ml1">
                         {goals && <Goals goals={goals} filter={goalFilters} displayCount={displayCount}></Goals>}
                     </div>

diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
@@ -227,7 +227,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
             />
             <div style={{ display: hasMessages ? 'block' : 'none' }} key="messages">
                 <Details initiallyOpen key="messages">
-                    <summary className="mv2 pointer">Messages ({messages.length})</summary>
+                    <>Messages ({messages.length})</>
                     <div className="ml1">
                         <MessagesList uri={pos.uri} messages={messages} />
                     </div>

diff --git a/lean4-infoview/src/infoview/messages.tsx b/lean4-infoview/src/infoview/messages.tsx
@@ -53,7 +53,7 @@ const MessageView = React.memo(({ uri, diag }: MessageViewProps) => {
     )
     return (
         <Details initiallyOpen>
-            <summary className={severityClass + ' mv2 pointer'}>
+            <span className={severityClass}>
                 {title}
                 <span className="fr" onClick={e => e.preventDefault()}>
                     <a
@@ -79,7 +79,7 @@ const MessageView = React.memo(({ uri, diag }: MessageViewProps) => {
                         title="copy message to clipboard"
                     ></a>
                 </span>
-            </summary>
+            </span>
             <div className="ml1" ref={node}>
                 <pre className="font-code pre-wrap">
                     <EnvPosContext.Provider value={startPos}>
@@ -192,7 +192,7 @@ export function AllMessages({ uri: uri0 }: { uri: DocumentUri }) {
     return (
         <RpcContext.Provider value={rs}>
             <Details setOpenRef={r => (setOpenRef.current = r)} initiallyOpen={!config.autoOpenShowsGoal}>
-                <summary className="mv2 pointer">
+                <>
                     All Messages ({numDiags ?? diags.length})
                     <span
                         className="fr"
@@ -211,7 +211,7 @@ export function AllMessages({ uri: uri0 }: { uri: DocumentUri }) {
                             title={isPaused ? 'continue updating' : 'pause updating'}
                         ></a>
                     </span>
-                </summary>
+                </>
                 <AllMessagesBody uri={uri} messages={iDiags} setNumDiags={setNumDiags} />
             </Details>
         </RpcContext.Provider>

diff --git a/lean4-infoview/src/infoview/tooltips.tsx b/lean4-infoview/src/infoview/tooltips.tsx
@@ -251,6 +251,7 @@ export function useHoverTooltip(
         clearTimeout()
         setState(state === 'pin' ? 'hide' : 'pin')
         e.stopPropagation()
+        e.preventDefault()
     }
 
     const onClick = (e: React.MouseEvent<HTMLSpanElement>) => {

diff --git a/lean4-infoview/src/infoview/traceExplorer.tsx b/lean4-infoview/src/infoview/traceExplorer.tsx
@@ -44,6 +44,7 @@ function LazyTrace({ col, cls, msg }: { col: number; cls: string; msg: MessageDa
                     void fetchTrace()
                     setOpen(true)
                     ev.stopPropagation()
+                    ev.preventDefault()
                 }}
             >
                 [{cls}] &gt;
@@ -57,6 +58,7 @@ function LazyTrace({ col, cls, msg }: { col: number; cls: string; msg: MessageDa
                     onClick={ev => {
                         setOpen(false)
                         ev.stopPropagation()
+                        ev.preventDefault()
                     }}
                 >
                     [{cls}] ∨
@@ -72,6 +74,7 @@ function LazyTrace({ col, cls, msg }: { col: number; cls: string; msg: MessageDa
                     onClick={ev => {
                         void fetchTrace()
                         ev.stopPropagation()
+                        ev.preventDefault()
                     }}
                 >
                     [{cls}] Error (click to retry):
@@ -134,6 +137,7 @@ function CollapsibleTraceNode(traceEmbed: TraceEmbed) {
             // Don't handle clicks within React portals nested in this div (notably, tooltips).
             if (!ev.currentTarget.contains(ev.target)) return
             ev.stopPropagation()
+            ev.preventDefault()
             if (!open) void fetchChildren()
             setOpen(o => !o)
         },