diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx index bf47a5ad7..f13bb6707 100644 --- 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([]) + // https://react.dev/learn/you-might-not-need-an-effect#adjusting-some-state-when-a-prop-changes + const [prevPos, setPrevPos] = React.useState(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) => { )} - +
<>Messages ({messages.length})