fun getImprovedTextRange()

in src/main/kotlin/org/arend/highlight/BasePass.kt [590:680]


        fun getImprovedTextRange(error: GeneralError?, element: PsiElement): TextRange {
            val improvedElement = getImprovedErrorElement(error, element) ?: element

            ((improvedElement as? ArendDefIdentifier)?.parent as? ArendDefinition<*>)?.let {
                return TextRange(it.textRange.startOffset, improvedElement.textRange.endOffset)
            }

            (((improvedElement as? ArendRefIdentifier)?.parent as? ArendLongName)?.parent as? ArendCoClause)?.let {
                return TextRange(it.textRange.startOffset, improvedElement.textRange.endOffset)
            }

            ((improvedElement as? ArendLongName)?.parent as? CoClauseBase)?.let { coClause ->
                val endElement = coClause.expr?.let { if (isEmptyGoal(it)) it else null } ?: coClause.fatArrow
                ?: coClause.lbrace ?: improvedElement
                return TextRange(coClause.textRange.startOffset, endElement.textRange.endOffset)
            }

            (improvedElement as? ArendGoal)?.let {
                if (it.expr != null) {
                    return TextRange(it.textRange.startOffset, improvedElement.textRange.endOffset)
                }
            }

            if ((error as? CertainTypecheckingError)?.kind == BODY_IGNORED) {
                (improvedElement as? ArendExpr ?: improvedElement.parent as? ArendExpr)?.let { expr ->
                    (expr.topmostEquivalentSourceNode.parentSourceNode as? ArendClause)?.let { clause ->
                        return TextRange((clause.fatArrow ?: expr).textRange.startOffset, expr.textRange.endOffset)
                    }
                }
            }

            if (improvedElement is ArendClause) {
                val prev = improvedElement.extendLeft.prevSibling
                val startElement = if (prev is LeafPsiElement && prev.elementType == PIPE) prev else improvedElement
                val endOffset =
                        if (error is ConditionsError) (improvedElement.patterns.lastOrNull() as? PsiElement
                                ?: improvedElement as PsiElement).textRange.endOffset
                        else improvedElement.textRange.endOffset
                return TextRange(startElement.textRange.startOffset, endOffset)
            }

            if ((error as? CertainTypecheckingError)?.kind == TOO_MANY_PATTERNS && improvedElement is ArendPattern) {
                var endElement: ArendPattern = improvedElement
                while (true) {
                    var next = endElement.extendRight.nextSibling
                    if (next is LeafPsiElement && next.elementType == COMMA) {
                        next = next.extendRight.nextSibling
                    }
                    if (next is ArendPattern) {
                        endElement = next
                    } else {
                        break
                    }
                }
                return TextRange(improvedElement.textRange.startOffset, endElement.textRange.endOffset)
            }

            if ((error is GoalError || error == null) && isIncomplete(improvedElement)) {
                if (improvedElement !is LeafPsiElement) {
                    val offset = improvedElement.textRange.endOffset
                    return TextRange(offset, offset + if (improvedElement.nextElement == null) 0 else 1)
                }

                var next = improvedElement.nextSibling
                if (next is PsiWhiteSpace) {
                    val text = next.text
                    val first = text.indexOf('\n')
                    if (first == -1) {
                        next = next.nextSibling
                    } else {
                        val second = text.indexOf('\n', first + 1)
                        val offset = next.textRange.startOffset
                        return if (second == -1) TextRange(offset + first + 1, offset + first + 2)
                        else TextRange(offset + second, offset + second + 1)
                    }
                }
                if (next != null) {
                    val offset = next.textRange.startOffset
                    return TextRange(offset, offset + 1)
                }
            }

            if (improvedElement is LeafPsiElement && STATEMENT_WT_KWS_TOKENS.contains(improvedElement.elementType)) {
                val stat = improvedElement.ancestor<ArendDefinition<*>>()?.parent
                if (stat != null) {
                    return TextRange(stat.startOffset, improvedElement.endOffset)
                }
            }

            return improvedElement.textRange
        }