This means that we can finally tweak server options on the fly!
We use the workspace/didChangeConfiguration notification, however note that our use is still very rudimentary (and push-based) when compared to the recommended pull model using the
workspace/configuration request.
This means that we can finally tweak server options on the fly!
We use the
workspace/didChangeConfiguration
notification, however note that our use is still very rudimentary (and push-based) when compared to the recommended pull model using theworkspace/configuration
request.