diff --git a/vscode/quint-vscode/CHANGELOG.md b/vscode/quint-vscode/CHANGELOG.md index 4e1ad18d0..140a486dd 100644 --- a/vscode/quint-vscode/CHANGELOG.md +++ b/vscode/quint-vscode/CHANGELOG.md @@ -12,6 +12,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Deprecated ### Removed ### Fixed + +- The language server should no longer crash when there is a crash on quint + functions (#1205) + ### Security ## v0.9.1 -- 2023-10-02 diff --git a/vscode/quint-vscode/server/src/parsing.ts b/vscode/quint-vscode/server/src/parsing.ts index 56382ce64..97af22e3c 100644 --- a/vscode/quint-vscode/server/src/parsing.ts +++ b/vscode/quint-vscode/server/src/parsing.ts @@ -23,26 +23,29 @@ export async function parseDocument(idGenerator: IdGenerator, textDocument: Text // see https://github.com/informalsystems/quint/issues/831 return new Promise((_resolve, reject) => reject(`Support imports from file, found: ${parsedUri.scheme}`)) } - - const result = parsePhase1fromText(idGenerator, text, parsedUri.path) - .chain(phase1Data => { - const resolver = fileSourceResolver() - const mainPath = resolver.lookupPath(dirname(parsedUri.fsPath), basename(parsedUri.fsPath)) - return parsePhase2sourceResolution(idGenerator, resolver, mainPath, phase1Data) - }) - .chain(phase2Data => parsePhase3importAndNameResolution(phase2Data)) - .chain(phase3Data => parsePhase4toposort(phase3Data)) - .mapLeft(messages => - messages.flatMap(msg => { - // TODO: Parse errors should be QuintErrors - const error: QuintError = { code: 'QNT000', message: msg.explanation, reference: 0n, data: {} } - return msg.locs.map(loc => assembleDiagnostic(error, loc)) + try { + const result = parsePhase1fromText(idGenerator, text, parsedUri.path) + .chain(phase1Data => { + const resolver = fileSourceResolver() + const mainPath = resolver.lookupPath(dirname(parsedUri.fsPath), basename(parsedUri.fsPath)) + return parsePhase2sourceResolution(idGenerator, resolver, mainPath, phase1Data) }) - ) + .chain(phase2Data => parsePhase3importAndNameResolution(phase2Data)) + .chain(phase3Data => parsePhase4toposort(phase3Data)) + .mapLeft(messages => + messages.flatMap(msg => { + // TODO: Parse errors should be QuintErrors + const error: QuintError = { code: 'QNT000', message: msg.explanation, reference: 0n, data: {} } + return msg.locs.map(loc => assembleDiagnostic(error, loc)) + }) + ) - if (result.isRight()) { - return new Promise((resolve, _reject) => resolve(result.value)) - } else { - return new Promise((_resolve, reject) => reject(result.value)) + if (result.isRight()) { + return new Promise((resolve, _reject) => resolve(result.value)) + } else { + return new Promise((_resolve, reject) => reject(result.value)) + } + } catch (e) { + return new Promise((_resolve, reject) => reject(e)) } } diff --git a/vscode/quint-vscode/server/src/server.ts b/vscode/quint-vscode/server/src/server.ts index 2b27bb1ca..c4080e10f 100644 --- a/vscode/quint-vscode/server/src/server.ts +++ b/vscode/quint-vscode/server/src/server.ts @@ -439,21 +439,26 @@ export class QuintLanguageServer { } private analyze(document: TextDocument, previousDiagnostics: Diagnostic[] = []) { - const parsedData = this.parsedDataByDocument.get(document.uri) - if (!parsedData) { - return - } + try { + const parsedData = this.parsedDataByDocument.get(document.uri) + if (!parsedData) { + return + } - const { modules, sourceMap, table } = parsedData + const { modules, sourceMap, table } = parsedData - this.docsByDocument.set(document.uri, new Map(modules.flatMap(m => [...produceDocsById(m).entries()]))) + this.docsByDocument.set(document.uri, new Map(modules.flatMap(m => [...produceDocsById(m).entries()]))) - const [errors, analysisOutput] = analyzeModules(table, modules) + const [errors, analysisOutput] = analyzeModules(table, modules) - this.analysisOutputByDocument.set(document.uri, analysisOutput) + this.analysisOutputByDocument.set(document.uri, analysisOutput) - const diagnostics = diagnosticsFromErrors(errors, sourceMap) - this.connection.sendDiagnostics({ uri: document.uri, diagnostics: previousDiagnostics.concat(diagnostics) }) + const diagnostics = diagnosticsFromErrors(errors, sourceMap) + this.connection.sendDiagnostics({ uri: document.uri, diagnostics: previousDiagnostics.concat(diagnostics) }) + } catch (e) { + this.connection.console.error(`Error during analysis: ${e}`) + this.connection.sendDiagnostics({ uri: document.uri, diagnostics: previousDiagnostics }) + } } }