Interest in deeper integration with Agda #35
Description
I've recently been dissatisfied with the state of Agda's editor support, so experimented with implementing a language server for it (and a basic client VS Code extension for testing).
The agda-language-server currently:
- interacts with Agda through the same interface as
agda-mode(except for hover) - exposes its behavior (primarily) through a custom LSP method
- does not implement most standard LSP requests
- implements the standard LSP hover request, but in a heuristic and overly simplistic way
By contrast, my experiment:
- integrates more closely with Agda, manually invoking the type checker, inspecting its state, and performing folds over abstract syntax to extract semantic information
- exposes its behavior through standard LSP requests
- does not implement any of the functionality of
agda-mode - implements the following LSP requests:
- Go to Declaration/Definition/References
- Document Highlight (highlight occurrences of the symbol under the cursor)
- Document Symbols (VS Code outline, search symbols within file)
- Hover (shows type of top-level definitions; type of local variables needs changes to Agda)
- Completions (currently half-baked, but much more should be possible)
Following this experiment, I'd like to file a series of PRs to integrate this functionality alongside the existing agda-mode functionality. It would make the server more complex, but much richer. I wanted to discuss before filing PRs for such large changes. Is there interest in this sort of functionality and server architecture?