I love the new ghost-highlighting feature in the Dafny extension. This feature adds a gray background for statements that are ghost. I have two further suggestions/wishes for this mode.

• I have found that lemma bodies are all grayed out. My first thought was that this is due lemmas always being ghost. However, in writing up this Issue, I'm finding that I can't always reproduce the situation. I have now written several lemma or least lemma declarations without their bodies being turned into gray, and I've also written some method bodies where the statements do turn gray (even for assignments to non-ghost out-parameters, which are definitely not ghost statements).

  Here's one example:

  

  So, my assessment is now that the feature is rather unreliable. I don't understand when it's recomputing this information or what to expect.

• The other issue I have is selected code doesn't show up over the gray ghost highlighting. Usually, when I select some code, it lights up with a blue background. But when the code is displayed as ghost, then the background remains gray even when I select some code. This feels wrong to me as a user. I would like the blue selection highlighting to take priority over the gray ghost highlighting.