Open Qiu233 opened 3 months ago
The language server is not involved here - the underlines and the Unicode mechanism are entirely client sided.
Some questions:
v0.0.124
, also note that I didn't restart vscode after switching the extension versionconsole.ts:137 [Extension Host] rejected promise not handled within 1 second: TypeError: Cannot read properties of undefined (reading 'dispose') C @ console.ts:137 console.ts:137 [Extension Host] stack trace: TypeError: Cannot read properties of undefined (reading 'dispose') at t.AbbreviationRewriterFeature.
(/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:159973) at Generator.next ( ) at s (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:158285) at processTicksAndRejections (node:internal/process/task_queues:95:5) C @ console.ts:137 mainThreadExtensionService.ts:81 [leanprover.lean4]Cannot read properties of undefined (reading 'dispose') $onExtensionRuntimeError @ mainThreadExtensionService.ts:81 mainThreadExtensionService.ts:82 TypeError: Cannot read properties of undefined (reading 'dispose') at t.AbbreviationRewriterFeature. (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:159973) at Generator.next ( ) at s (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:158285) at processTicksAndRejections (node:internal/process/task_queues:95:5) $onExtensionRuntimeError @ mainThreadExtensionService.ts:82 console.ts:137 [Extension Host] rejected promise not handled within 1 second: TypeError: Cannot read properties of undefined (reading 'dispose') C @ console.ts:137 console.ts:137 [Extension Host] stack trace: TypeError: Cannot read properties of undefined (reading 'dispose') at t.AbbreviationRewriterFeature. (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:159973) at Generator.next ( ) at s (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:158285) at processTicksAndRejections (node:internal/process/task_queues:95:5) C @ console.ts:137 mainThreadExtensionService.ts:81 [leanprover.lean4]Cannot read properties of undefined (reading 'dispose') $onExtensionRuntimeError @ mainThreadExtensionService.ts:81 mainThreadExtensionService.ts:82 TypeError: Cannot read properties of undefined (reading 'dispose') at t.AbbreviationRewriterFeature. (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:159973) at Generator.next ( ) at s (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:158285) at processTicksAndRejections (node:internal/process/task_queues:95:5)
also note that I didn't restart vscode after switching the extension version
You should! Or at least click the "Restart Extensions" button that shows up in the extension entry after the update. Otherwise it will still use the previous version.
Could you also double-check that the issue indeed does not occur with Lean v4.8.0 on v0.0.170 of the extension?
(By the way, the error you saw above is likely unrelated but will be fixed by #492. Thanks for the report.)
Are you still encountering this issue?
It's almost solved now. But sometimes unicode fails, leave it as is and the bottom panel of vscode shows up with errors. Redoing it will fix.
There's another cursor issue which I am not sure related to this issue or not.
For example, when typing \times
I usually got ×
but with cursor on the left of it.
This happens more often when typing faster, especially working in codespace remotely.
But sometimes unicode fails, leave it as is and the bottom panel of vscode shows up with errors.
What is the error you are seeing and what is your current vscode-lean4 version?
FWIW, the fact that replacing the abbreviation sometimes fails is unfortunately something we can't fix (VS Code doesn't support transactions for updating editor state, so if the editor state has changed since the abbreviation mechanism was called, VS Code simply rejects our edits to the document).
There's another cursor issue which I am not sure related to this issue or not.
For this issue, it would also be good to know what your vscode-lean4 version is. We fixed this issue a while ago unless you are also using the Vim extension, in which case text edits issued by the Vim extension and vscode-lean4 can interfere.
Sometimes the backslash symbol
\
become plain text rather with an underline indicating it's pending further input. To fix it I must either:I have been experiencing this problem very often since updating to 4.9.0, on both macos and windows with wsl. The cause isn't clear. I tried different vscode extension versions published months ago but the problem still remains, so the language server is more likely to have caused this.