From 05f809026e42cd68fb8fc01b3e523dc4607fdd7e Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 6 Sep 2024 09:30:55 -0500 Subject: [PATCH] Chore: Code to debug 5753 --- .../DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs index 59801b3a02..17f9af50bc 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs @@ -1005,6 +1005,12 @@ method test() { var documentItem = CreateTestDocument(source, "OpeningDocumentWithTimeoutReportsTimeoutDiagnostic.dfy"); client.OpenDocument(documentItem); var diagnostics = await GetLastDiagnostics(documentItem); + if (diagnostics.Length > 1) { + throw new Exception( + "There should be only one diagnostic, got :" + + string.Join(", ", diagnostics.Select(diagnostic => diagnostic.ToString() + "(" + diagnostic.Message + ")")) + ); + } Assert.Single(diagnostics); Assert.Contains("timed out", diagnostics[0].Message); }