Some way to hide non-generating code

[ajewellamz]

Just a pipe dream -- I'd really like a couple of keystrokes :

One hides/shows all comments
One hides/shows all requires, ensures, assert, assume, invariant and the like.

If I use both, I'm able to see just the code that actually translates into running code in the target language, which in many cases is difficult to see through all the noise.

Of course, if that becomes one or several commands, that's fine too.

Any hope for something like that?

[keyboardDrummer]

Folding of lines, which VSCode supports, comes close to what you're asking for, although in folding there's always one remaining line.

I think for comments the folding should suffice, although it's currently not working for Dafny files. The Dafny server could register an LSP folding range provider and that should fix it reliably.

For ghost-code, I don't think folding would provide a good user interface. VSCode also supports virtual documents. You would invoke something like "show executed code" and it would open another tab that only shows the non-ghost code in your previous file (I would suggest with foldable comments), but you likely wouldn't be able to edit it because it's a one-way projection.

So, what you're asking for is not a pipe dream, but when we'll have time for that I can't say. I don't think it will be any time soon.