We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
See diff in this PR: hhu-adam/monaco-lean4#1
Overview of diff:
lean
lean4
webview/index.ts
Addressed:
leanclient.ts
collectAllOpenLeanDocumentUris
projectInfo.ts
findLeanProjectRootInfo
clientProvider.ts
checkIsLeanVersionUpToDate
vscode.css
_serverProcess
infoview.ts
InfoProvider
setInfoviewElement
batch.ts
fsHelper.ts
spawn
promises
ambiguous indirect export
memfs
abbreviations.json
_character
character
taskgutter.ts
logger.ts
Console
The text was updated successfully, but these errors were encountered:
No branches or pull requests
See diff in this PR: hhu-adam/monaco-lean4#1
Overview of diff:
lean
first and then tolean4
?webview/index.ts
] Loading scripts was easier using imports, but might be possible using the loader as wellAddressed:
leanclient.ts
]collectAllOpenLeanDocumentUris
does not work as expectedprojectInfo.ts
]findLeanProjectRootInfo
requires filesystemclientProvider.ts
] Checks require file system (e.g.checkIsLeanVersionUpToDate
)vscode.css
] Stylesheet variables are provided to VSCode webviews automatically. We need to inject it into the iframe by hand.webview/index.ts
] Communication works differently in IFrameleanclient.ts
] Use Monaco Language Client instead of VSCode Language Client_serverProcess
in leanclient. leanprover/vscode-lean4#487infoview.ts
] WebviewPanel in gets replaced by HTMLIFrameElementInfoProvider
getssetInfoviewElement
function to supply location of infoviewbatch.ts
/fsHelper.ts
]spawn
/promises
cannot be imported:ambiguous indirect export
: usingmemfs
nowVite fails to load(Fixed: 1ce695c)abbreviations.json
properly[(Fixed: hhu-adam/monaco-lean4@40fa306)infoview.ts
] Editor.selection for some reason uses_character
instead ofcharacter
.fix: do not implicitely cast Position to ls.Position. leanprover/vscode-lean4#486[(Fixed: hhu-adam/monaco-lean4@2a01c47)taskgutter.ts
] Adjust image paths[logger.ts
] Console object seems to work differentlyConsole
in hhu-adam/monaco-lean4@bd9197b.The text was updated successfully, but these errors were encountered: