The lean.nvim project uses a single buffer for the infoview for all buffers. If implemented in agda, this would allow for switching between agda buffers (:bn) or switching between tabs (:tabnext) while and not having redundant infoviews.
The lean.nvim developer gave the following code pointers for this feature: where lean.nvim updates the infoview and where it switches the owning buffer.
The lean.nvim project uses a single buffer for the infoview for all buffers. If implemented in agda, this would allow for switching between agda buffers (
:bn) or switching between tabs (:tabnext) while and not having redundant infoviews.The lean.nvim developer gave the following code pointers for this feature: where lean.nvim updates the infoview and where it switches the owning buffer.