Ghost diagnostics not correctly updated

[MikaelMayer]

Dafny version

4.3.0

Code to produce this issue

class A {
}


method Test(a: object) {
  if a is A {
  }
}

Command to run and resulting output

Paste the code above in VS Code.
The lines `if a is A {}` are highlighted in ghost correctly.
Now, inside the braces, write
`print "hello";`
Now delete lines 3-5, and press enter 6 times to reproduce the animated screenshot below.

What happened?

What's going on

• There is no more ghost code in the code, and the language server does not send a notification to the client. Hence, the client does not know that there is no more ghost code and continues to highlight the region of previous ghost code as ghost.
• You can verify this hypothesis by writing another method that contains ghost code, immediately the ghost code is updated.

What type of operating system are you experiencing the problem on?

Windows