The LSP server in lsp-server.ML does not use the HOL parser currently. It should be updated to track intermediate states based on work in hol4-vscode.
This issue is complete when there is enough functionality in the LSP server to implement an editor mode for a new editor (including for example reimplementing the VSCode mode without writing any SML code).
The LSP server in
lsp-server.MLdoes not use the HOL parser currently. It should be updated to track intermediate states based on work in hol4-vscode.This issue is complete when there is enough functionality in the LSP server to implement an editor mode for a new editor (including for example reimplementing the VSCode mode without writing any SML code).