Request textDocument/completion failed.

[kevinsullivan]

As I'm working along on a few pretty simple Dafny files in the VS Code extension, I repeatedly get the following error. I am posting here to document the issue, and will update this issue as I gain insight into the conditions that lead to this error.

OS = OSX High Sierra (10.13) Plugin version = 0.10.10 Dafny version = Hard to tell, no obvious -version compiler option, but current as of January 2018

[Error - 13:14:26] Request textDocument/completion failed. Message: Request textDocument/completion failed with message: Cannot read property 'getText' of undefined Code: -32603

[bxie]

also getting this error. actual result: UI shows my dafny code being verified without errors when errors are certainly present (as verified on rise4fun). expected: verification fails and errors, failures shown because dafny code has bugs

OS = OSX Sierra (10.12) Plugin version = 0.11.1 VS Code v 1.23.1

[Error - 14:17:37] Request textDocument/definition failed. Message: Request textDocument/definition failed with message: Cannot read property 'then' of null Code: -32603

as an aside, I ran this on another machine which is running OSX High Sierra and I didn't have this bug.

[hexchain]

I had no problem with the extension until I killed DafnyServer once, then I ran into this. Code actions are also gone.

[fabianhauser]

@kevinsullivan @bxie @sorawee @hexchain Could you check if you still experience this bug in the current release (0.17.0)? The problem was probably fixed in 0e499bf3b86424204ee6eb9e18dbd020a22ad9ae.

[hexchain]

Unfortunately yes, I still experience this bug.