Large span for while loop informational message causes UI overload

[jaylorch]

When using the verus-analyzer plugin in VS Code, if there's an informational message about a while loop like while loop: not all errors may have been reported; rerun with a higher value for --multiple-errors..., the associated span is the entire while loop including all invariants and the body. This causes it to all be underlined in blue squiggles in VS Code, which makes it very difficult to work with. Could you please change this informational message to only span the keyword while?

See illustration below.