The first commit makes the server aware of the options tracked by the vscode extension. when server::run gets called, it makes an initial request for the user's stored preferences, and after that it will ask for them again when it gets a notification of an update. According to this issue you're not supposed to/able to get the actual config contents by using the change notification, hence the two-step process.
The struct/enum approach for the options is a little bit heavy, but I think in conjunction with the serde macros it's less error prone.
The second commit is a rework of the elaborate on save thing that applies changes eagerly (and can now be toggled in the vscode extension settings for Metamath Zero). The two window/workspace edge case works fine this way. I left it so that hover will always elaborate since it needs the spans to match what users are seeing, but I changed document_symbol and completion_resolve to try and fetch an old environment iff the user wants to elaborate on save, since they trigger often enough to negate the usefulness of elab on save otherwise.
The first commit makes the server aware of the options tracked by the vscode extension. when
server::rungets called, it makes an initial request for the user's stored preferences, and after that it will ask for them again when it gets a notification of an update. According to this issue you're not supposed to/able to get the actual config contents by using the change notification, hence the two-step process.The struct/enum approach for the options is a little bit heavy, but I think in conjunction with the serde macros it's less error prone.
The second commit is a rework of the elaborate on save thing that applies changes eagerly (and can now be toggled in the vscode extension settings for Metamath Zero). The two window/workspace edge case works fine this way. I left it so that hover will always elaborate since it needs the spans to match what users are seeing, but I changed document_symbol and completion_resolve to try and fetch an old environment iff the user wants to elaborate on save, since they trigger often enough to negate the usefulness of elab on save otherwise.