Fixes gutter when cache is enabled

[MikaelMayer]

Fixes dafny-lang/ide-vscode#187

The issue was that caching would prevent reports of implementations being finished to verify for the gutter reporting mechanism. I added it, and a test that I verified would not work in the absence of the fix.

Changes

• It also report all the results that were cached as if they were resolved immediately.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[MikaelMayer]

Before the fix, the last [O] and [=] would have been replaced by [ ] because the result of individual cached splits were not reported the second time.

[MikaelMayer]

Before the fix, this text would not terminate because it would never get back to the | icon

[keyboardDrummer]

I find having two methods ReportAssertionBatchResult to be confusing. What do you think?

Seems like you could also change AssertionBatchResult so it contains only an Implementation and a VCResult

[MikaelMayer]

The first signature makes something nice, it's possible assign AssertionBatchResults to their correct implementation in a threaded way:

dafny/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs

Lines 136 to 137 in 07d614f

	var subscription = verifier.BatchCompletions.Where(c =>
	implementations.Contains(c.Split.Implementation)).Subscribe(progressReporter.ReportAssertionBatchResult);

The second signature is the one I need because I don't have the split available, only the implementation and the result from the cache.

I just pushed something I'm satisfied with: I removed the split from AssertionBatchResult and just included the Implementation because we are not using other properties of the split anyway.