LSP: completion, document outline, documentation hovers, tests#1371

Open

ciaran-matthew-dunne wants to merge 14 commits into

Deducteam:masterfrom

ciaran-matthew-dunne:pr/lsp-ux

Commits on Jul 9, 2026

parser: map a bare open to P_open again
ciaran-matthew-dunne
committed
LSP: success hints on the ";" of commands and the keyword of tactics
ciaran-matthew-dunne
committed
LSP: review fixes for success hint positions
ciaran-matthew-dunne
committed
LSP: show command success hints on the introducing keyword
ciaran-matthew-dunne
committed
LSP groundwork: expose command AST, module-path ranges, printer state
ciaran-matthew-dunne
committed
LSP: robust message framing and JSON-RPC replies
ciaran-matthew-dunne
committed
LSP: initialize reads workspace folders and client capabilities
ciaran-matthew-dunne
committed
LSP: hierarchical document symbols
ciaran-matthew-dunne
committed
LSP: go-to-definition on module paths, with in-scope fallback
ciaran-matthew-dunne
committed
LSP: keyword documentation and hypothesis types on hover
ciaran-matthew-dunne
committed
parser: expose the tokens acceptable at the end of a source prefix
ciaran-matthew-dunne
committed
LSP: grammar-driven completion
ciaran-matthew-dunne
committed
LSP: integration test suite (make test_lsp)
ciaran-matthew-dunne
committed
add CHANGES.md entry
ciaran-matthew-dunne
committed