Trigger synchronous analysis for completion

informalsystems · Sep 13, 2023 · ea330e0 · ea330e0
1 parent dbc503c
commit ea330e0
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 12 deletions.
diff --git 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<string, DocumentationEntry>
 ): 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
@@ -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<DocumentSymbol[], void> => {
@@ -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