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
}