You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
;(this.client as any)._serverProcess.stderr.on('data', async (chunk: Buffer) => {
...
})
When adapting the extension to monaco, we are replacing vscode's LanguageClient (link to source) with the MonacoLanguageClient (link to source) which does not have _serverProcess, so we basically delete the marked code snippet.
As (this.client as any)._serverProcess seems like quite a hack already (i.e. _serverProcess is marked private), I thought I'd mark this here. Maybe there is a better way to do this that would work in both cases?
The text was updated successfully, but these errors were encountered:
Consider the following lines of code:
https://github.com/leanprover/vscode-lean4/blob/cee53169b58d31a03a60c4769ee827a3cabffd7c/vscode-lean4/src/leanclient.ts#L264C1-L274C11
When adapting the extension to monaco, we are replacing vscode's
LanguageClient
(link to source) with theMonacoLanguageClient
(link to source) which does not have_serverProcess
, so we basically delete the marked code snippet.As
(this.client as any)._serverProcess
seems like quite a hack already (i.e._serverProcess
is markedprivate
), I thought I'd mark this here. Maybe there is a better way to do this that would work in both cases?The text was updated successfully, but these errors were encountered: