in src/main/kotlin/org/arend/refactoring/ArendRefactoringUtils.kt [184:226]
fun execute(editor: Editor?) {
val parent = element.parent
val factory = ArendPsiFactory(element.project)
val id = if (newName.size > 1 && target != null && useOpen &&
doAddIdToOpen(factory, newName, element, target)) singletonList(newName.last()) else newName
val needsModification = element.longName != id
when (element) {
is ArendIPName -> if (parent is ArendLiteral) {
if (!needsModification) return
val argumentStr = buildString {
if (id.size > 1) {
append(LongName(id.dropLast(1)))
append(".")
}
if (element.fixity == Fixity.INFIX || element.fixity == Fixity.POSTFIX) append("`")
append(id.last())
if (element.fixity == Fixity.INFIX) append("`")
}
val replacementLiteral = factory.createExpression(argumentStr).descendantOfType<ArendLiteral>()
if (replacementLiteral != null) parent.replace(replacementLiteral)
}
else -> {
val longNameStr = LongName(id).toString()
val longNameStartOffset = element.parent.textOffset
val relativePosition = max(0, (editor?.caretModel?.offset ?: 0) - longNameStartOffset)
val offset = max(0, relativePosition + LongName(id).toString().length - LongName(element.longName).toString().length)
val longName = factory.createLongName(longNameStr)
if (needsModification) {
when (parent) {
is ArendLongName -> {
parent.addRangeAfter(longName.firstChild, longName.lastChild, element)
parent.deleteChildRange(parent.firstChild, element)
}
is ArendPattern -> element.replace(longName)
}
editor?.caretModel?.moveToOffset(longNameStartOffset + offset)
}
}
}
}