[Feature request]: Reduce "file contains no code" messages

[RustanLeino]

What is the feature you would like to see in a future version of Dafny?

Given an empty file, Dafny reports "file contains no code". This was introduced to alert users of files they thought were nonempty, but where they accidentally had commented out the actual contents of the body. This message is only of marginal value, so one could consider removing it altogether. Here is a proposal for how we can both reduce spurious warnings of this sort and still cater for the original use case:

Report "file contains no code" when both of the following apply:

• The file contains nothing but comments
• There is at least one /* ... */ comment in the file

[MikaelMayer]

This message was introduced because the first syntax highlighter was not taking into account nested comments, and comments don't need to be finished. So the following would make it seems Dafny could prove false.

/* /* ooops */
method Aha() ensures false {
}

This is no longer the case at least in VSCode. So I think we can remove the message even in your cases you mention.