Error messages don't respect the infoview context order

Stream: lean4

[Yaël Dillies]

Have people noticed this? Errors show context (eg "unsolved goals") in the default order even when the context order is set to reverse.

[Julian Berman]

I'm not in front of Lean but my recollection is that the diagnostic message comes from the server preassembled

[Julian Berman]

Whereas the goal state VSCode assembles and respects the setting

[Julian Berman]

Which isn't to say this isn't fixable but yeah if my recollection is right then I think the backend isn't seeing the setting today

[Yaël Dillies]

I guess my question is "Should I open an issue?"

[Julian Berman]

I guess yes though I suspect priority-wise it wouldn't get immediate attention. I think even more broadly it might be worth considering if diagnostic messages from the server should be "as structured" as the goal state is normally -- i.e. if the goal state wasn't "pre-rendered" as a string. The LSP spec does have some spots where diagnostic objects can put arbitrary structured data -- https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#diagnostic