diff --git a/src/language/api/verificationGutterStatusParams.ts b/src/language/api/verificationGutterStatusParams.ts index c21a19fa..2cc8230c 100644 --- a/src/language/api/verificationGutterStatusParams.ts +++ b/src/language/api/verificationGutterStatusParams.ts @@ -1,3 +1,4 @@ + import { DocumentUri, integer } from 'vscode-languageclient'; export interface IVerificationGutterStatusParams { diff --git a/src/language/api/verificationSymbolStatusParams.ts b/src/language/api/verificationSymbolStatusParams.ts index fca58cc9..45db24e7 100644 --- a/src/language/api/verificationSymbolStatusParams.ts +++ b/src/language/api/verificationSymbolStatusParams.ts @@ -15,6 +15,6 @@ export enum PublishedVerificationStatus { Stale = 0, // Not scheduled to be run Queued = 1, // Scheduled to be run but waiting for resources Running = 2, // Currently running - Error = 4, // Finished and had errors - Correct = 5 // Finished and was correct + Error = 3, // Finished and had errors + Correct = 4 // Finished and was correct } \ No newline at end of file diff --git a/src/language/dafnyLanguageClient.ts b/src/language/dafnyLanguageClient.ts index 895cd198..cc3c3383 100644 --- a/src/language/dafnyLanguageClient.ts +++ b/src/language/dafnyLanguageClient.ts @@ -7,10 +7,10 @@ import { DafnyDocumentFilter } from '../tools/vscode'; import { ICompilationStatusParams, IVerificationCompletedParams, IVerificationStartedParams } from './api/compilationStatus'; import { ICounterexampleItem, ICounterexampleParams } from './api/counterExample'; import { IGhostDiagnosticsParams } from './api/ghostDiagnostics'; -import { IVerificationGutterStatusParams as IVerificationGutterStatusParams } from './api/verificationGutterStatusParams'; import { IVerificationSymbolStatusParams } from './api/verificationSymbolStatusParams'; import { DafnyInstaller } from './dafnyInstallation'; import * as os from 'os'; +import { IVerificationGutterStatusParams } from './api/verificationGutterStatusParams'; const LanguageServerId = 'dafny-vscode'; const LanguageServerName = 'Dafny Language Server'; @@ -28,13 +28,15 @@ function getLanguageServerLaunchArgsNew(): string[] { const specifiedCores = parseInt(Configuration.get(ConfigurationConstants.LanguageServer.VerificationVirtualCores)); // This is a temporary fix to prevent 0 cores from being used, since the languages server currently does not handle 0 cores correctly: https://github.com/dafny-lang/dafny/pull/3276 const cores = isNaN(specifiedCores) || specifiedCores === 0 ? Math.ceil((os.cpus().length + 1) / 2) : Math.max(1, specifiedCores); + const displayGutterIcons = Configuration.get(ConfigurationConstants.LanguageServer.DisplayGutterStatus); return [ `--verify-on:${verifyOn}`, `--verification-time-limit:${Configuration.get(ConfigurationConstants.LanguageServer.VerificationTimeLimit)}`, getVerifierCachingPolicy(), `--cores:${cores}`, `--notify-ghostness:${Configuration.get(ConfigurationConstants.LanguageServer.MarkGhostStatements)}`, - `--notify-line-verification-status:${Configuration.get(ConfigurationConstants.LanguageServer.DisplayGutterStatus)}`, + '--notify-line-verification-status:false', + `--show-assertions:${displayGutterIcons ? 'All' : 'Implicit'}`, ...getDafnyPluginsArgument(), ...launchArgs ]; diff --git a/src/test/suite/extension.test.ts b/src/test/suite/extension.test.ts index d74c08c2..91df59f9 100644 --- a/src/test/suite/extension.test.ts +++ b/src/test/suite/extension.test.ts @@ -13,6 +13,8 @@ import { Messages } from '../../ui/messages'; import { DafnyCommands } from '../../commands'; import VerificationGutterStatusView from '../../ui/verificationGutterStatusView'; import { DocumentSymbol } from 'vscode'; +import { PublishedVerificationStatus } from '../../language/api/verificationSymbolStatusParams'; +import { LineVerificationStatus } from '../../language/api/verificationGutterStatusParams'; const mockedWorkspace = MockingUtils.mockedWorkspace(); const mockedVsCode = { @@ -143,6 +145,236 @@ suite('Verification Gutter', () => { assert.deepStrictEqual([ new vscode.Range(7, 1, 8, 1) ], ranges.get(2)); assert.deepStrictEqual([ new vscode.Range(3, 1, 3, 1), new vscode.Range(5, 1, 5, 1) ], ranges.get(0)); }); + + test('computeGutterIconsParseError', () => { + const source = ` +method Foo() { + parse(;)Error +} + +method Bat() + ensures false +{ + if (true) { + return; + } else { + return; + } +} + +method Fom() { + assert true; +}`.trimStart(); + const uri = vscode.Uri.parse('file:///woops.dfy'); + const parseError = new vscode.Diagnostic(new vscode.Range(1, 2, 1, 15), 'Some parse error', vscode.DiagnosticSeverity.Error); + parseError.source = 'Parser'; + const outdatedReturnError = new vscode.Diagnostic(new vscode.Range(8, 8, 8, 14), 'Outdated: a postcondition could not be proved on this return path', vscode.DiagnosticSeverity.Warning); + outdatedReturnError.relatedInformation = [ { + location: { uri, range: new vscode.Range(5, 14, 5, 19) }, + message: 'This postcondition might not hold: false' + } ]; + const expected = [ + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.ResolutionError, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.AssertionFailedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.AssertionFailedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete + ]; + const computedIcons = VerificationGutterStatusView.computeGutterIcons( + virtualDocument(uri, source), + false, undefined, undefined, [ + parseError, + outdatedReturnError + ] + ); + assert.deepStrictEqual(expected, computedIcons); + }); + + function virtualDocument(uri: vscode.Uri, source: string): vscode.TextDocument { + const lines = source.split('\n'); + return { + uri: uri, + getText: (range: vscode.Range) => { + return lines[range.start.line]; + }, + lineCount: lines.length + } as vscode.TextDocument; + } + + test('foundAllError', () => { + const source = ` +method Faz() { + assert true; + assert true; + assert false; // Error +}`.trimStart(); + const computedIcons = VerificationGutterStatusView.computeGutterIcons( + virtualDocument(vscode.Uri.parse('file:///woops.dfy'), source), + false, new Map([ + [ '0,7', new vscode.Range(0, 0, 4, 1) ] + ]), [ + { nameRange: new vscode.Range(0, 7, 0, 10), status: PublishedVerificationStatus.Error } + ], [ + new vscode.Diagnostic(new vscode.Range(3, 2, 3, 14), 'could not prove assertion', vscode.DiagnosticSeverity.Error) + ]); + const expected = [ + LineVerificationStatus.Nothing, + LineVerificationStatus.AssertionVerifiedInErrorContext, + LineVerificationStatus.AssertionVerifiedInErrorContext, + LineVerificationStatus.AssertionFailed, + LineVerificationStatus.AssertionVerifiedInErrorContext + ]; + assert.deepStrictEqual(expected, computedIcons); + }); + + test('computeGutterIconsResolved', () => { + const source = ` +method Foo() { // Stale + assert false; // No error +} + +method Bat() { // Stale + assert false; // Outdated error +} + +method Bar() { // Queued + assert false; +} + +method Baz() { // Running + assert false; +} + +method Fom() { // Correct + assert true; +} + +method Faz() { // Error + assert true; + assert false; // Error +}`.trimStart(); + const computedIcons = VerificationGutterStatusView.computeGutterIcons( + virtualDocument(vscode.Uri.parse('file:///woops.dfy'), source), + true, new Map([ + [ '0,7', new vscode.Range(0, 0, 2, 1) ], + [ '4,7', new vscode.Range(4, 0, 6, 1) ], + [ '8,7', new vscode.Range(8, 0, 10, 1) ], + [ '12,7', new vscode.Range(12, 0, 14, 1) ], + [ '16,7', new vscode.Range(16, 0, 18, 1) ], + [ '20,7', new vscode.Range(20, 0, 23, 1) ] + ]), [ + { nameRange: new vscode.Range(0, 7, 0, 10), status: PublishedVerificationStatus.Stale }, + { nameRange: new vscode.Range(4, 7, 4, 10), status: PublishedVerificationStatus.Stale }, + { nameRange: new vscode.Range(8, 7, 8, 10), status: PublishedVerificationStatus.Queued }, + { nameRange: new vscode.Range(12, 7, 12, 10), status: PublishedVerificationStatus.Running }, + { nameRange: new vscode.Range(16, 7, 16, 10), status: PublishedVerificationStatus.Correct }, + { nameRange: new vscode.Range(20, 7, 20, 10), status: PublishedVerificationStatus.Error } + ], [ + new vscode.Diagnostic(new vscode.Range(5, 2, 5, 14), 'Outdated: could not prove assertion', vscode.DiagnosticSeverity.Warning), + new vscode.Diagnostic(new vscode.Range(17, 2, 17, 14), 'some warning', vscode.DiagnosticSeverity.Warning), + Object.assign(new vscode.Diagnostic(new vscode.Range(21, 2, 21, 12), 'Assertion: division', vscode.DiagnosticSeverity.Hint), + { code: 'isAssertion' }), + new vscode.Diagnostic(new vscode.Range(22, 2, 22, 14), 'could not prove assertion', vscode.DiagnosticSeverity.Error) + ]); + const expected = [ + LineVerificationStatus.Nothing, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.Verified, + LineVerificationStatus.Nothing, + LineVerificationStatus.AssertionFailedObsolete, + LineVerificationStatus.ErrorContextObsolete, + LineVerificationStatus.Verified, + LineVerificationStatus.Nothing, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.Verified, + LineVerificationStatus.Nothing, + LineVerificationStatus.VerifiedVerifying, + LineVerificationStatus.VerifiedVerifying, + LineVerificationStatus.Verified, + LineVerificationStatus.Nothing, + LineVerificationStatus.Verified, + LineVerificationStatus.Verified, + LineVerificationStatus.Verified, + LineVerificationStatus.Nothing, + LineVerificationStatus.AssertionVerifiedInErrorContext, + LineVerificationStatus.AssertionFailed, + LineVerificationStatus.ErrorContext + ]; + assert.deepStrictEqual(expected, computedIcons); + }); + + + test('foundSomeErrorsTrackAssertions', () => { + const source = ` +method FoundSomeErrors() { + if (*) { + assert false; + } else { + var x := 3 / 2; + } + assert false; +} +method FoundAllErrors() { + if (*) { + assert false; + } else { + var x := 3 / 2; + } + assert true; +}`.trimStart(); + const computedIcons = VerificationGutterStatusView.computeGutterIcons( + virtualDocument(vscode.Uri.parse('file:///woops.dfy'), source), + true, new Map([ + [ '0,7', new vscode.Range(0, 0, 7, 1) ], + [ '8,7', new vscode.Range(8, 0, 15, 1) ] + ]), [ + { nameRange: new vscode.Range(0, 7, 0, 22), status: PublishedVerificationStatus.Error }, + { nameRange: new vscode.Range(8, 7, 8, 21), status: PublishedVerificationStatus.Error } + ], [ + Object.assign(new vscode.Diagnostic(new vscode.Range(0, 7, 0, 22), 'Verification hit error limit so not all errors may be shown.', + vscode.DiagnosticSeverity.Error), { code: 'errorLimitHit' }), + new vscode.Diagnostic(new vscode.Range(2, 4, 2, 16), 'could not prove assertion', vscode.DiagnosticSeverity.Error), + Object.assign(new vscode.Diagnostic(new vscode.Range(4, 4, 4, 16), 'Assertion: division', vscode.DiagnosticSeverity.Hint), + { code: 'isAssertion' }), + new vscode.Diagnostic(new vscode.Range(6, 4, 6, 18), 'could not prove assertion', vscode.DiagnosticSeverity.Error), + new vscode.Diagnostic(new vscode.Range(10, 4, 10, 16), 'could not prove assertion', vscode.DiagnosticSeverity.Error), + Object.assign(new vscode.Diagnostic(new vscode.Range(12, 4, 12, 18), 'Assertion: division', vscode.DiagnosticSeverity.Hint), + { code: 'isAssertion' }) + ]); + const expected = [ + LineVerificationStatus.Nothing, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.AssertionFailed, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.AssertionFailed, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.Nothing, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.AssertionFailed, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.AssertionVerifiedInErrorContext, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.AssertionVerifiedInErrorContext, + LineVerificationStatus.ErrorContext + ]; + assert.deepStrictEqual(expected, computedIcons); + }); }); suite('commands', () => { diff --git a/src/ui/dafnyIntegration.ts b/src/ui/dafnyIntegration.ts index f24ea02f..0cb2c557 100644 --- a/src/ui/dafnyIntegration.ts +++ b/src/ui/dafnyIntegration.ts @@ -24,7 +24,10 @@ export default function createAndRegisterDafnyIntegration( if(serverSupportsSymbolStatusView && Configuration.get(ConfigurationConstants.LanguageServer.DisplayVerificationAsTests)) { symbolStatusView = VerificationSymbolStatusView.createAndRegister(installer.context, languageClient); } - VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusView); + const displayGutterStatus = Configuration.get(ConfigurationConstants.LanguageServer.DisplayGutterStatus); + if(displayGutterStatus) { + VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusView); + } CompileCommands.createAndRegister(installer); RelatedErrorView.createAndRegister(installer.context, languageClient); DafnyVersionView.createAndRegister(installer, languageServerVersion); diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index 5f657707..bc8b836b 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -1,5 +1,5 @@ /* eslint-disable max-depth */ -import { Range, window, ExtensionContext, workspace, TextEditor, TextEditorDecorationType, Uri } from 'vscode'; +import { Range, TextDocument, window, ExtensionContext, workspace, TextEditor, TextEditorDecorationType, Uri, Position, DocumentSymbol, Diagnostic, DiagnosticSeverity, commands, languages } from 'vscode'; import { Disposable } from 'vscode-languageclient'; import { IVerificationGutterStatusParams, @@ -11,6 +11,7 @@ import { import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; import { getVsDocumentPath } from '../tools/vscode'; import VerificationSymbolStatusView from './verificationSymbolStatusView'; +import { NamedVerifiableStatus, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; const DELAY_IF_RESOLUTION_ERROR = 2000; const ANIMATION_INTERVAL = 200; @@ -57,7 +58,8 @@ export default class VerificationGutterStatusView { private static readonly emptyLinearVerificationDiagnostics: Map = VerificationGutterStatusView.FillLineVerificationStatusMap(); - private constructor(context: ExtensionContext, private readonly symbolStatusView: VerificationSymbolStatusView | undefined) { + private constructor(context: ExtensionContext, + private readonly symbolStatusView: VerificationSymbolStatusView | undefined) { const icon = VerificationGutterStatusView.makeIconAux(false, context); const grayIcon = VerificationGutterStatusView.makeIconAux(true, context); const lvs = LineVerificationStatus; @@ -114,14 +116,191 @@ export default class VerificationGutterStatusView { languageClient: DafnyLanguageClient, symbolStatusView: VerificationSymbolStatusView | undefined): VerificationGutterStatusView { const instance = new VerificationGutterStatusView(context, symbolStatusView); + languageClient.onPublishDiagnostics((uri) => { + instance.update(uri); + }); + context.subscriptions.push( workspace.onDidCloseTextDocument(document => instance.clearVerificationDiagnostics(document.uri.toString())), window.onDidChangeActiveTextEditor(editor => instance.refreshDisplayedVerificationGutterStatuses(editor)), - languageClient.onVerificationStatusGutter(params => instance.updateVerificationStatusGutter(params)) + workspace.onDidChangeTextDocument(e => { + if(instance.lineCountsPerDocument.get(e.document.uri) !== e.document.lineCount) { + instance.update(e.document.uri); + } + }) ); + if(symbolStatusView !== undefined) { + context.subscriptions.push( + symbolStatusView.onUpdates(uri => { + instance.update(uri); + }) + ); + } return instance; } + private readonly lineCountsPerDocument = new Map(); + private async update(uri: Uri) { + const rootSymbols = await commands.executeCommand('vscode.executeDocumentSymbolProvider', uri) as DocumentSymbol[] | undefined; + const nameToSymbolRange = rootSymbols === undefined ? undefined : this.getNameToSymbolRange(rootSymbols); + const diagnostics = languages.getDiagnostics(uri); + const verifiableRanges = this.symbolStatusView!.getVerifiableRangesForUri(uri); + + const document = await workspace.openTextDocument(uri); + + this.lineCountsPerDocument.set(document.uri, document.lineCount); + const perLineStatus = VerificationGutterStatusView.computeGutterIcons(document, true, nameToSymbolRange, verifiableRanges, diagnostics); + this.updateUsingLineStatus({ uri: uri.toString(), perLineStatus: perLineStatus }); + } + + private getNameToSymbolRange(rootSymbols: DocumentSymbol[]): Map { + const result = new Map(); + const stack = rootSymbols; + while(stack.length > 0) { + const top = stack.pop()!; + const children = top.children ?? []; + stack.push(...children); + result.set(positionToString(top.selectionRange.start), top.range); + } + return result; + } + + // eslint-disable-next-line max-params + public static computeGutterIcons( + document: TextDocument, + assertionTracking: boolean, + nameToSymbolRanges: Map | undefined, + statuses: NamedVerifiableStatus[] | undefined, + diagnostics: Diagnostic[]): LineVerificationStatus[] { + const statusPerLine = new Map(); + const lineToErrorSource = new Map(); + const lineToSymbolRange = new Map(); + const linesInErrorContext = new Set(); + const linesToSkip = new Set(); + const implicitAssertionLines = new Set(); + const errorLimitHitVerifiables = new Set(); + + if(nameToSymbolRanges !== undefined) { + for(const range of nameToSymbolRanges.values()) { + for(let line = range.start.line; line < range.end.line; line++) { + lineToSymbolRange.set(line, range); + } + } + } + const perLineStatus: LineVerificationStatus[] = []; + for(const diagnostic of diagnostics) { + if(diagnostic.code === 'errorLimitHit') { + errorLimitHitVerifiables.add(positionToString(diagnostic.range.start)); + } + + const assertionMarker = diagnostic.code === 'isAssertion'; + if(assertionMarker) { + // Just the first line of the assertion is sufficient. + implicitAssertionLines.add(diagnostic.range.start.line); + } + + const outdatedError = diagnostic.message.startsWith('Outdated: '); + if(diagnostic.severity !== DiagnosticSeverity.Error && !outdatedError) { + continue; + } + + const source = diagnostic.source ?? ''; + for(const related of diagnostic.relatedInformation ?? []) { + if(related.location.uri === document.uri) { + processErrorRange(related.location.range, source); + } + } + processErrorRange(diagnostic.range, source); + } + + if(nameToSymbolRanges === undefined || statuses === undefined) { + for(let line = 0; line < document.lineCount; line++) { + statusPerLine.set(line, { progress: PublishedVerificationStatus.Stale, hitErrorLimit: false }); + } + } else { + for(const status of statuses) { + const convertedRange = VerificationSymbolStatusView.convertRange(status.nameRange); + const positionString = positionToString(convertedRange.start); + const hitErrorLimit = errorLimitHitVerifiables.has(positionString); + const symbolRange = nameToSymbolRanges.get(positionToString(convertedRange.start)); + linesToSkip.add(convertedRange.start.line); + if(symbolRange === undefined) { + console.error('symbol mismatch between documentSymbol and symbolStatus API'); + continue; + } + const lineStatus = { progress: status.status, hitErrorLimit: hitErrorLimit }; + for(let line = symbolRange.start.line; line <= symbolRange.end.line; line++) { + statusPerLine.set(line, lineStatus); + } + } + } + + function processErrorRange(range: Range, source: string | undefined) { + for(let line = range.start.line; line <= range.end.line; line++) { + lineToErrorSource.set(line, source ?? ''); + const contextRange = lineToSymbolRange.get(line); + if(contextRange === undefined) { + continue; + } + for(let contextLine = contextRange.start.line; contextLine <= contextRange.end.line; contextLine++) { + linesInErrorContext.add(contextLine); + } + } + } + + for(let line = 0; line < document.lineCount; line++) { + if(linesToSkip.has(line)) { + perLineStatus.push(LineVerificationStatus.Nothing); + continue; + } + + const lineText = document.getText(new Range(line, 0, line + 1, 0)); + const isExplicitAssertion = lineText.trimStart().startsWith('assert'); + + const error = lineToErrorSource.get(line); + if(error === 'Parser' || error === 'Resolver') { + perLineStatus.push(LineVerificationStatus.ResolutionError); + } else { + const lineStatus = statusPerLine.get(line)!; + let resultStatus: number; + if(error !== undefined) { + resultStatus = LineVerificationStatus.AssertionFailed; + } else { + if(linesInErrorContext.has(line)) { + const considerLineAsHavingAssertions + = !assertionTracking || implicitAssertionLines.has(line) || isExplicitAssertion; + if(lineStatus?.hitErrorLimit === false && considerLineAsHavingAssertions) { + // If we found all errors then an assertion with no error must be correct. + resultStatus = LineVerificationStatus.AssertionVerifiedInErrorContext; + } else { + resultStatus = LineVerificationStatus.ErrorContext; + } + } else { + resultStatus = LineVerificationStatus.Verified; + } + } + let progressStatus: number; + switch(lineStatus?.progress) { + case PublishedVerificationStatus.Stale: + case PublishedVerificationStatus.Queued: + progressStatus = GutterIconProgress.Stale; + break; + case PublishedVerificationStatus.Running: + progressStatus = GutterIconProgress.Running; + break; + case PublishedVerificationStatus.Error: + case PublishedVerificationStatus.Correct: + case undefined: + progressStatus = GutterIconProgress.Done; + break; + default: throw new Error(`unknown PublishedVerificationStatus ${statusPerLine.get(line)}`); + } + perLineStatus.push(resultStatus + progressStatus); + } + } + return perLineStatus; + } + /// Creation of an decoration type private static iconOf(context: ExtensionContext, path: string, grayMode: boolean): TextEditorDecorationType { const icon = context.asAbsolutePath(`images/${path}.png`); @@ -265,7 +444,7 @@ export default class VerificationGutterStatusView { const symbolParams = params.perLineStatus.indexOf(LineVerificationStatus.ResolutionError) > 0 ? [] : (this.symbolStatusView?.getVerifiableRangesForUri(uri) ?? []); - const originalLinesToSkip = symbolParams.map(range => range.start.line).sort((a, b) => a - b); + const originalLinesToSkip = symbolParams.map(range => range.nameRange.start.line).sort((a, b) => a - b); return VerificationGutterStatusView.perLineStatusToRanges(perLineStatus, originalLinesToSkip); } @@ -309,7 +488,7 @@ export default class VerificationGutterStatusView { } // Entry point when receiving IVErificationStatusGutter - private updateVerificationStatusGutter(params: IVerificationGutterStatusParams) { + private updateUsingLineStatus(params: IVerificationGutterStatusParams) { if(this.areParamsOutdated(params)) { return; } @@ -398,4 +577,14 @@ export default class VerificationGutterStatusView { } } } -} \ No newline at end of file +} + +export enum GutterIconProgress { + Stale = 1, + Running = 2, + Done = 0 +} + +function positionToString(start: Position): string { + return `${start.line},${start.character}`; +} diff --git a/src/ui/verificationSymbolStatusView.ts b/src/ui/verificationSymbolStatusView.ts index fbabf619..1b007a0b 100644 --- a/src/ui/verificationSymbolStatusView.ts +++ b/src/ui/verificationSymbolStatusView.ts @@ -1,7 +1,7 @@ /* eslint-disable max-depth */ -import { commands, ExtensionContext, workspace, tests, Range, Position, Uri, TestRunRequest, TestController, TestRun, DocumentSymbol, TestItem, TestItemCollection, TextDocument, TestRunProfileKind } from 'vscode'; +import { commands, ExtensionContext, workspace, Event, tests, Range, Position, Uri, TestRunRequest, TestController, TestRun, DocumentSymbol, TestItem, TestItemCollection, TextDocument, TestRunProfileKind, EventEmitter } from 'vscode'; import { Range as lspRange, Position as lspPosition } from 'vscode-languageclient'; -import { IVerificationSymbolStatusParams, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; +import { IVerificationSymbolStatusParams, NamedVerifiableStatus, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; class ResolveablePromise { @@ -39,6 +39,15 @@ export default class VerificationSymbolStatusView { return new VerificationSymbolStatusView(context, languageClient); } + private itemStates: Map = new Map(); + private itemRuns: Map = new Map(); + private readonly runItemsLeft: Map = new Map(); + private readonly controller: TestController; + private automaticRunEnd: boolean = false; + private noRunCreationInProgress: Promise = Promise.resolve(); + private readonly _onUpdates: EventEmitter = new EventEmitter(); + public onUpdates: Event = this._onUpdates.event; + public constructor( private readonly context: ExtensionContext, private readonly languageClient: DafnyLanguageClient) { @@ -50,12 +59,6 @@ export default class VerificationSymbolStatusView { ); } - private itemStates: Map = new Map(); - private itemRuns: Map = new Map(); - private readonly runItemsLeft: Map = new Map(); - private readonly controller: TestController; - private automaticRunEnd: boolean = false; - private noRunCreationInProgress: Promise = Promise.resolve(); private createController(): TestController { const controller = tests.createTestController('verificationStatus', 'Verification Status'); @@ -127,6 +130,7 @@ export default class VerificationSymbolStatusView { await this.noRunCreationInProgress; const uri = Uri.parse(params.uri); + await this.noRunCreationInProgress; params.uri = uri.toString(); const document = await workspace.openTextDocument(uri); const rootSymbols = await commands.executeCommand('vscode.executeDocumentSymbolProvider', uri) as DocumentSymbol[] | undefined; @@ -167,6 +171,7 @@ export default class VerificationSymbolStatusView { controller.items.add(leafItem); } } + this._onUpdates.fire(document.uri); const allTestItems: TestItem[] = []; function collectTestItems(collection: TestItemCollection) { @@ -193,6 +198,8 @@ export default class VerificationSymbolStatusView { const newItemRuns = new Map(); params.namedVerifiables.forEach((element, index) => { const testItem = leafItems[index]; + this.statuses.set(testItem.id, element.status); + const itemRunState = this.itemRuns.get(testItem.id)!; if(this.itemStates.get(testItem.id) === element.status) { const isRunning = itemRunState !== undefined; @@ -310,7 +317,6 @@ export default class VerificationSymbolStatusView { return item; } - public static convertRange(range: lspRange): Range { return new Range( VerificationSymbolStatusView.convertPosition(range.start), @@ -321,15 +327,18 @@ export default class VerificationSymbolStatusView { return new Position(position.line, position.character); } - public getVerifiableRangesForUri(uri: Uri): Range[] { + private readonly statuses: Map = new Map(); + + public getVerifiableRangesForUri(uri: Uri): NamedVerifiableStatus[] { const stack: TestItemCollection[] = [ this.controller.items ]; - const ranges: Range[] = []; + const ranges: NamedVerifiableStatus[] = []; while(stack.length !== 0) { const top = stack.pop()!; top.forEach(child => { - if(child.uri === uri) { - if(child.range !== undefined) { - ranges.push(child.range); + if(child.uri?.toString() === uri.toString()) { + const status = this.statuses.get(child.id); + if(child.range !== undefined && status !== undefined) { + ranges.push({ nameRange: child.range, status: status }); } stack.push(child.children); }