fun execute()

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)
                }
            }
        }
    }