UI: verbose data and warnings not printed at the right place/moment

[fblanqui]

verbose 3;
symbol A:TYPE;// the log panel should display: "(symb) A : TYPE" instead of nothing currently
symbol a:A;// the log panel should display: "(symb) a : A" instead of "(symb) A : TYPE" currently

[fblanqui]

Hello @firewall2142 . Would you have some time to look at this problem too?

[fblanqui]

See tests/OK/admit.lp. There are several problems:

Emacs:

• if we do Ctrl+C & Ctrl+C on the first admitted, we get no warnings
• to get them we need to do Ctrl+C Ctrl+N
• at the end of the file, we never get the warnings for the last proof (to see them, wee need to add a new command, say "symbol A:TYPE;")

VSCode:

• in contrast with Emacs, semi-colons are not included in the green zone
• doing Ctrl+Right from the beginning, we get only "begi" in green
• if we do Ctrl+Right and Ctrl+Left, "begin" is in green
• same behavior than Emacs on warnings: if we do 2 times Ctrl+Right, we get the warnings for the previous admitted at the end of the file, we never get the warnings for the last proof (to see them, you need to a new command, say "symbol A:TYPE;")

[firewall2142]

I think it might be a good idea to move the proof navigation code to the LSP server and keep the code for the editor extensions to a minimum. This will be helpful in avoiding the off-by-one errors.

[fblanqui]

@firewall2142 Could you please elaborate? How would you proceed?

[firewall2142]

Currently, vscode and emacs look for terminators like "begin", ";" in the file's content. We could make changes so that the LSP server provides the position of the terminators.