diff --git a/vscode/quint-vscode/server/src/complete.ts b/vscode/quint-vscode/server/src/complete.ts index c6d21bb34..8c9db93ee 100644 --- a/vscode/quint-vscode/server/src/complete.ts +++ b/vscode/quint-vscode/server/src/complete.ts @@ -2,6 +2,7 @@ import { compact } from 'lodash' import { MarkupContent } from 'vscode-languageclient' import { CompletionItem, CompletionItemKind, MarkupKind, Position } from 'vscode-languageserver/node' import { + AnalysisOutput, DocumentationEntry, IRVisitor, ParserPhase3, @@ -11,7 +12,6 @@ import { QuintLambda, QuintModule, QuintType, - analyzeModules, booleanOperators, findDefinitionWithId, findExpressionWithId, @@ -30,22 +30,20 @@ import { findMatchingResults } from './reporting' export function completeIdentifier( identifier: string, parsedData: ParserPhase3, + analysisOutput: AnalysisOutput, sourceFile: string, position: Position, builtinDocs: Map ): CompletionItem[] { - const { modules, table } = parsedData + const { table } = parsedData // Until we have incremental parsing, try to lookup `triggeringIdentifier` by name const declIds = findDeclByNameAtPos(identifier, position, sourceFile, parsedData) - // FIXME: use analysisOutputByDocument - const [_, aop] = analyzeModules(table, modules) - // Lookup types for the found declarations const types = declIds.map(declId => { const refId = table.get(declId)?.id ?? declId - return aop.types.get(refId)?.type + return analysisOutput.types.get(refId)?.type }) const properTypes = compact( types.map(type => { diff --git a/vscode/quint-vscode/server/src/server.ts b/vscode/quint-vscode/server/src/server.ts index d11ee9401..2b27bb1ca 100644 --- a/vscode/quint-vscode/server/src/server.ts +++ b/vscode/quint-vscode/server/src/server.ts @@ -269,10 +269,15 @@ export class QuintLanguageServer { return [] } + const document = this.documents.get(params.textDocument.uri) + if (!document) { + return [] + } + // Parse the identifier that triggered completion // TODO: offer completion for chained calls // (e.g., `tup._2.`, `rec.field.` or `set.powerset().`) - const triggeringLine = documents.get(params.textDocument.uri)?.getText({ + const triggeringLine = document.getText({ start: { ...params.position, character: 0 }, end: params.position, }) @@ -285,7 +290,22 @@ export class QuintLanguageServer { const sourceFile = URI.parse(params.textDocument.uri).path - return completeIdentifier(triggeringIdentifier, parsedData, sourceFile, params.position, loadedBuiltInDocs) + // Run analysis synchronously to get the required information for completion + this.triggerAnalysis(document) + + const analysisOutput = this.analysisOutputByDocument.get(params.textDocument.uri) + if (!analysisOutput) { + return [] + } + + return completeIdentifier( + triggeringIdentifier, + parsedData, + analysisOutput, + sourceFile, + params.position, + loadedBuiltInDocs + ) }) connection.onDocumentSymbol((params: DocumentSymbolParams): HandlerResult => { @@ -403,18 +423,22 @@ export class QuintLanguageServer { this.analysisOutputByDocument.delete(uri) } + private triggerAnalysis(document: TextDocument, previousDiagnostics: Diagnostic[] = []) { + clearTimeout(this.analysisTimeout) + this.connection.console.info(`Triggering analysis`) + this.analyze(document, previousDiagnostics) + } + private scheduleAnalysis(document: TextDocument, previousDiagnostics: Diagnostic[] = []) { clearTimeout(this.analysisTimeout) const timeoutMillis = 1000 this.connection.console.info(`Scheduling analysis in ${timeoutMillis} ms`) this.analysisTimeout = setTimeout(() => { - this.analyze(document, previousDiagnostics).catch(err => - this.connection.console.error(`Failed to analyze: ${err.message}`) - ) + this.analyze(document, previousDiagnostics) }, timeoutMillis) } - private async analyze(document: TextDocument, previousDiagnostics: Diagnostic[] = []) { + private analyze(document: TextDocument, previousDiagnostics: Diagnostic[] = []) { const parsedData = this.parsedDataByDocument.get(document.uri) if (!parsedData) { return