chore: truncate error messages endPos

@Kha, @Vtec234, @mhuisi:
This is a bit hackish, but it improves the usuability quite a bit in
VS Code. Without this hack, I often get huge blocks of "red squiggly lines".

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