dafny-lang / ide-vscode

VSCode IDE Integration for Dafny
https://marketplace.visualstudio.com/items?itemName=dafny-lang.ide-vscode
MIT License
23 stars 18 forks source link

Error "Request textDocument/documentSymbol failed" appears regularly #446

Closed tchajed closed 11 months ago

tchajed commented 11 months ago

While typing out code (so with many intermediate states with invalid code, and possibly due to concurrency) I very often get this error:

[Error - 12:00:38 PM] Request textDocument/documentSymbol failed.
Error: Illegal argument: line must be non-negative
    at w (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/workbench/api/node/extensionHostProcess.js:10:1101)
    at new s (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/workbench/api/node/extensionHostProcess.js:121:4368)
    at new o (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/workbench/api/node/extensionHostProcess.js:121:5884)
    at D (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:429900)
    at W (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:435434)
    at W (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:435547)
    at W (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:435547)
    at d (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:473826)
    at Object.t.map (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:473912)
    at Object.asDocumentSymbols (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:443428)
    at r (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:379675)
    at r.provideDocumentSymbols (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/workbench/api/node/extensionHostProcess.js:127:37581)

I'm using v3.2.1 of the extension and Dafny v4.3.0, and I'm on macOS.

keyboardDrummer commented 11 months ago

Any chance you could post a piece of code that causes this? I'm guessing it's a deterministic error.

tchajed commented 11 months ago

Sure, open up a new Dafny file and type function, then wait for a second.

keyboardDrummer commented 11 months ago

Sure, open up a new Dafny file and type function, then wait for a second.

Thank you! Fixed on master now