fix(lsp): Do not mark the bodies of lemmas as ghost.

[camrein]

Resolves dafny-lang/ide-vscode#126 by explicitly excluding lemmas when traversing the AST to collect ghost statements.

Taking this a step further: Since @RustanLeino couldn't always reproduce the issue, I suspect there's more than just lemmas being highlighted. I have two things in mind that could lead to the situation that the bug is not easily reproducible:

GhostStateDiagnosticCollector runs even when the resolution failed. See TextDocumentLoader. The reported ghost statement in the AST might be incorrect due to this. The fix would be quite easy here: Only report ghost states for documents that resolved successfully. However, if that was the case, the error should surface not only within lemmas.

The other thing that might be worth a thought is the situation when the document moves into migrated state. That happens when the currently processed change is being canceled by a newer change. The language server then relocates the symbol table as well as the diagnostics according to this change (see DocumentDatabase). We'd either need to relocate the ghost diagnostics or discard them. Otherwise, I believe they might show invalid locations.

[cpitclaudel]

But aren't lemmas in fact ghost? I think it's not a bad thing to gray them out.
dafny-lang/ide-vscode#126 complained about incorrect highlighting, but didn't advocate for not highlighting lemmas, did it?

[camrein]

The motivation to not highlight the bodies comes from this discussion: dafny-lang/ide-vscode#53 (comment)
We opted to not highlight ghost statements in contexts where the statements are always ghost. That's why I've created this PR to no longer highlight lemmas.

Of course, it doesn't resolve highlighting statements falsely. To resolve this issue, I'll need more information. I'm pretty positive that the issue relates to one of the reasons I've outlined in the PR, or even both. I hope someone who's a more frequent Dafny user may confirm my assumptions before I (or someone else) start implementing potential fixes.

[MikaelMayer]

With the new italicized and slightly transparent highlighting of ghost statements, I think it makes sense that we don't mark the body of lemmas as ghost in our current mode where we already don't display something as ghost if it's in a ghost context anyway. While writing a lot of lemmas in VSCode recently, I would have really appreciated to have natural highlighting rather than italicized highlighting.
However, down the road, I really think it should be an option. Newcomers in Dafny should see everything that is ghost highlighted in ghost even if it's not ambiguous, that way, they can quickly learn the difference. Intermediate and expert users should be able to configure VSCode to have the current disambiguation-only highlighting.

[MikaelMayer]

I'm willing to help finish to merge this PR @camrein let me know how I can help !