Make incomplete proofs more prominent

[DanielFabian]

I've been working through mathematics in lean and I've found on the same page multiple incomplete proofs that I just didn't notice.

As it stands it puts a red squiggly under the by for a the tactics block.

It's pretty small and somewhat easy to miss.

How hard would it be to add something more prominent like the yellow squiggly when a proof uses sorry?

Maybe it's yellow when it uses sorry and red if it does not type check?

What are the thoughts on this.

[PatrickMassot]

I fully agree, and this is an issue for teaching especially. My workaround is to use the Error Lens VSCode extension, but this shouldn't be required.

[Kha]

We already have the progress indicator, projecting errors and other diagnostics onto that as well seems like a natural solution to me. Not sure if this should be changed in the server, as the client already has all relevant data for doing so.