open fun printUsageEntryInternal()

in src/main/kotlin/org/arend/refactoring/changeSignature/entries/UsageEntry.kt [105:161]


    open fun printUsageEntryInternal(
        globalReferable: GlobalReferable?,
        newParameters: List<ParameterDescriptor>,
        parameterMap: MutableMap<ParameterDescriptor, ArgumentPrintResult?>,
        hasExplicitExternalArgument: Boolean,
        argumentStartIndex: Int,
        doubleBuilder: DoubleStringBuilder): Pair<Boolean, Boolean> {
        val defClassMode = descriptor?.getAffectedDefinition() is ArendDefClass
        val lambdaParams = getLambdaParams(parameterMap.keys, false)
        val oldArgToLambdaArgMap = HashMap<ParameterDescriptor, String>()
        var lambdaArgs = ""
        val referables = ArrayList<Variable>()

        if (lambdaParams.isNotEmpty()) {
            val context = contextPsi.scope.elements.map { VariableImpl(it.textRepresentation()) }
            lambdaParams.forEach {
                val freshName = StringRenamer().generateFreshName(VariableImpl(it.getNameOrUnderscore()), context + referables)
                referables.add(VariableImpl(freshName))
                lambdaArgs += if (it.isExplicit) " $freshName" else " {$freshName}"
                oldArgToLambdaArgMap[it] = freshName
            }
        }

        val isLambda = lambdaArgs != "" && !defClassMode && this !is PatternEntry
        if (isLambda) doubleBuilder.append("\\lam$lambdaArgs => ")
        for (e in oldArgToLambdaArgMap) parameterMap[e.key] =
            ArgumentPrintResult(IntermediatePrintResult(if (this is PatternEntry) "_" else e.value, null, true, false, null), true, null)

        val printedFirstParameter = newParameters.firstOrNull()?.oldParameter?.let { parameterMap[it]?.printResult }
        val dotNotationSupported = newParameters.isNotEmpty() && newParameters.first().isThis() && printedFirstParameter?.text?.let { isIdentifier(it) } == true
                && target !is ArendConstructor /* <-- This is due to a small bug in Arend scopes */

        val startIndex = if (printedFirstParameter != null && dotNotationSupported && descriptor?.moveRefactoringContext == null) {
            doubleBuilder.append(printedFirstParameter.text)
            doubleBuilder.append(".")
            doubleBuilder.append(target?.refName!!)
            1
        } else {
            val contextName = getContextName()
            doubleBuilder.append(contextName, if (globalReferable?.precedence?.isInfix == true) "($contextName)" else contextName)
            0
        }

        val lastParameter = newParameters.lastOrNull { parameterMap[it.oldParameter] != null && !oldArgToLambdaArgMap.contains(it.oldParameter) }
        val lastIndex = if (lastParameter != null) newParameters.indexOf(lastParameter) else -1
        val relevantSegment = if (defClassMode) newParameters.subList(startIndex, lastIndex + 1) else newParameters.subList(startIndex, newParameters.size)
        var isAtomicExpression = !printParams(globalReferable, relevantSegment, lambdaParams, parameterMap, hasExplicitExternalArgument, doubleBuilder)

        var j = argumentStartIndex
        while (j < getArguments().size) {
            doubleBuilder.append(" ${getArguments()[j].printResult.text}")
            j++
            isAtomicExpression = false
        }

        return Pair(isAtomicExpression, isLambda)
    }