search

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
158 stars 48 forks source link

fix: do not implicitely cast Position to ls.Position. #486

Closed joneugster closed 3 months ago

joneugster commented 3 months ago

Adapting teh VSCode extension for monaco, there is an error message caused by this implicit typecast from Position to ls.Position:

Error updating: Error fetching goals: Rpc error: ParseError:
Cannot parse request params: {"textDocument":
{"uri":"file:///workspace/test.lean"},"sessionId":"1430986504474938216",
"position":{},"params"
{"textDocument":{"uri":"file:///workspace/test.lean"},"position":{}},
"method":"Lean.Widget.getInteractiveGoals"} Lean.Lsp.RpcCallParams.position:
Lean.Lsp.Position.line: Natural number expected. Try again.

I don't understand why this is, but apparently that's one way to fix it. (note: Position comes from the package @codingame/monaco-vscode-api in our setup and from VSCode in the normal setup. They should be identical.

abentkamp commented 3 months ago

I think what's happening is this: Position.line and Position.character are implemented as a getter (https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Functions/get) in monaco-vscode-api. When we send the position to the "webview" (in our case an iframe), the object gets serialized and loses the getter function.

We could also try to raise an issue with the authors of monaco-vscode-api. Not sure if they would consider this a bug.

EDIT: It's actually a getter in VSCode, too: https://github.com/microsoft/vscode/blob/main/src/vs/workbench/api/common/extHostTypes.ts#L149. Maybe the serialization for the webview works differently from the iframe?