From 142d6cbcbc04a8173635318427311b646e8ffd7f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Mar 2021 16:44:33 -0800 Subject: [PATCH] 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 | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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