diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean
index d2744731da..f703be85e0 100644
--- a/src/Lean/Data/Lsp/Diagnostics.lean
+++ b/src/Lean/Data/Lsp/Diagnostics.lean
@@ -90,7 +90,14 @@ structure PublishDiagnosticsParams where
 def msgToDiagnostic (text : FileMap) (m : Message) : IO Diagnostic := do
   let low : Lsp.Position := text.leanPosToLspPos m.pos
   let high : Lsp.Position := match m.endPos with
-    | some endPos => text.leanPosToLspPos endPos
+    | some endPos =>
+      /-
+        Truncate messages that are more than one line long.
+        This is a workaround to avoid big blocks of "red squiggly lines" on VS Code.
+        TODO: should it be a parameter?
+      -/
+      let endPos := if endPos.line > m.pos.line then { line := m.pos.line + 1, column := 0 } else endPos
+      text.leanPosToLspPos endPos
     | none        => low
   let range : Range := ⟨low, high⟩
   let severity := match m.severity with