From 03a651e6a3415e48f78ecba557a6deda3ba44ce1 Mon Sep 17 00:00:00 2001 From: enigmurl <43832426+enigmurl@users.noreply.github.com> Date: Mon, 21 Oct 2024 11:16:37 -0700 Subject: [PATCH] Clip diagnostic hints past certain length --- src/main/kotlin/lean4ij/language/InlayHints.kt | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/main/kotlin/lean4ij/language/InlayHints.kt b/src/main/kotlin/lean4ij/language/InlayHints.kt index 86e1eeb..367d337 100644 --- a/src/main/kotlin/lean4ij/language/InlayHints.kt +++ b/src/main/kotlin/lean4ij/language/InlayHints.kt @@ -410,7 +410,17 @@ class InlayTextAttributes: UnmodifiableTextAttributes() { } -class InlayRenderer(info: HighlightInfo): HintRenderer(info.description) { +class InlayRenderer(info: HighlightInfo): HintRenderer(clipDescription(info.description)) { + companion object { + const val MAX_LEN = 140; + fun clipDescription(desc: String): String { + return if (desc.length < MAX_LEN) { + desc + } else { + desc.substring(0, MAX_LEN - 3) + "..." + } + } + } override fun getTextAttributes(editor: Editor): TextAttributes? { return InlayTextAttributes() }