fix: widget persistence (#535)

Ensure that that user widgets are not remounted when the cursor moves, so that their component state persists.
leanprover · Oct 17, 2024 · 4ffed87 · 4ffed87
1 parent 32036f9
commit 4ffed87
Showing 1 changed file with 8 additions and 7 deletions.
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
@@ -131,6 +131,13 @@ function GoalInfoDisplay(props: GoalInfoDisplayProps) {
 
     const [selectedLocs, setSelectedLocs] = React.useState<GoalsLocation[]>([])
 
+    // https://react.dev/learn/you-might-not-need-an-effect#adjusting-some-state-when-a-prop-changes
+    const [prevPos, setPrevPos] = React.useState<DocumentPosition>(pos)
+    if (!DocumentPosition.isEqual(pos, prevPos)) {
+        setPrevPos(pos)
+        setSelectedLocs([])
+    }
+
     const locs: Locations = React.useMemo(
         () => ({
             isSelected: (l: GoalsLocation) => selectedLocs.some(v => GoalsLocation.isEqual(v, l)),
@@ -218,13 +225,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                     </a>
                 </div>
             )}
-            <GoalInfoDisplay
-                key={DocumentPosition.toString(pos)}
-                pos={pos}
-                goals={goals}
-                termGoal={termGoal}
-                userWidgets={userWidgets}
-            />
+            <GoalInfoDisplay pos={pos} goals={goals} termGoal={termGoal} userWidgets={userWidgets} />
             <div style={{ display: hasMessages ? 'block' : 'none' }} key="messages">
                 <Details initiallyOpen key="messages">
                     <>Messages ({messages.length})</>