From 2333a3fbabcbc2be1affe3bb54013edb28f4eda2 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Wed, 30 Dec 2020 17:56:53 -0500 Subject: [PATCH] fix: error responses in tests --- src/Lean/Data/Lsp/Ipc.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Lean/Data/Lsp/Ipc.lean b/src/Lean/Data/Lsp/Ipc.lean index 63f7c51ce4..408999933f 100644 --- a/src/Lean/Data/Lsp/Ipc.lean +++ b/src/Lean/Data/Lsp/Ipc.lean @@ -56,10 +56,12 @@ partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : let rec loop : IpcM (List (Notification PublishDiagnosticsParams)) := do match ←readMessage with | Message.response id _ => + if id == waitForDiagnosticsId then [] + else loop + | Message.responseError id code msg _ => if id == waitForDiagnosticsId then - [] - else - loop + throw $ userError s!"Waiting for diagnostics failed: {msg}" + else loop | Message.notification "textDocument/publishDiagnostics" (some param) => match fromJson? (toJson param) with | some diagnosticParam => ⟨"textDocument/publishDiagnostics", diagnosticParam⟩ :: (←loop)