Statement starting location is off

[RustanLeino]

In the VS Code IDE, I see

The Repr field is ghost, so note that most of the assignment statement is visually indicated as being ghost. However, the cv. part of the statement is not. I suspect this is because the statement .Tok doesn't give the start location of the statement.

I'm reporting this issue here, as opposed to in dafny-lang/ide-vscode, because I suspect the IDE just uses the .Tok field of the assignment statement.

Possible fix

I think the fix is to change the UpdateStmt<out Statement/*!*/ s> production in Dafny.atg to make it start off with var start = la; and then use this start instead of x in the various s = new ... at the end of the production. After that, the x is probably no longer needed.

I don't think this .Tok for various kinds of update statements is used for anything else, so I don't think this change will affect anything other than the ghost highlighting in the IDE.

[davidcok]

My experimentation indicates that the parser produces the correct token (at least as of now).