overturetool
Outline isn't always updated
This isn't very high priority, but I've noticed that the "outline" view of a spec isn't always updated when you might think it would. For example, if you have a saved/checked spec and then you add (say) a new "value" definition, you might expect that to appear in the outline when you save/check the spec again. But it doesn't... it appears as soon as you type another character after saving.
What seems to be happening is that the VSC client sends regular "documentSymbol" requests when you edit the spec, but it does not regard saving the spec as a "change" and so does not ask at that point. Unfortunately, the VDM tools only populate a full type-checked view of the spec - ie. including the new definition(s) - on a save.
You can also sometimes see a related problem where the outline view falls back to using untypechecked data (rather than nothing) when the spec has type checking errors. The outline in this case has names, but without the extra type information, like function params and return types. When the spec is corrected, the outline stays untyped until you start typing, when it flips into the full typed version.
So I just wanted to record/explain this, in case others see the problem. It's tricky to fix though, unless we can find a way to get the client to ask for documentSymbols on a save.
I think it should be fairly easy to make the client do a documentSymbols request on save. I might be able to check it tomorrow.
OK, that would be a nice solution if it's possible. I can't see a way for the server to provoke the client into making a documentSymbols otherwise!
Hm.. It seems i am able to send the message and receive the document symbols, however this only seems possible when going around the VSCode API, with the result that the Outline view is not updated..
According to: https://github.com/microsoft/vscode/issues/108722 and https://github.com/Microsoft/vscode/issues/71454 we are not the only ones who would like an ability to update the outline, but I don't think it is possible right now. However, it has been moved to the VSCode backlog, so we might get it later on.
OK, thanks for looking into it. It's not super critical: either a spec isn't being changed and there's no problem, or you're actively changing something, in which case as soon as you type a character after a save, it updates so there's no (big) problem.
We can keep an eye on VSC updates to see whether a feature like this becomes available. But let's leave this issue open so that anyone who notices will understand the status.