in src/main/kotlin/org/arend/refactoring/changeSignature/ArendParametersInfo.kt [38:98]
fun parameterText(): String {
data class TeleEntry(val typeText: String?, val isExplicit: Boolean, val isCoerce: Boolean, val isClassifying: Boolean, val isProperty: Boolean, val accessModifier: org.arend.term.group.AccessModifier = org.arend.term.group.AccessModifier.PUBLIC, val parameterNames: MutableList<Pair<String?, Int>>)
val teleEntries = ArrayList<TeleEntry>()
val associatedWhitespaceData = HashSet<Pair<TeleEntry, TeleWhitespaceData>>()
val usedWhitespaceData = HashSet<TeleWhitespaceData>()
for (parameter in parameterInfo) {
if (teleEntries.isEmpty() || teleEntries.last().typeText != parameter.typeText || teleEntries.last().isExplicit != parameter.isExplicit() || parameter.isCoerce || parameter.isClassifying)
teleEntries.add(TeleEntry(parameter.typeText, parameter.isExplicit(), parameter.isCoerce, parameter.isClassifying, parameter.isProperty, parameter.accessModifier, Collections.singletonList(
Pair(parameter.name, parameter.oldIndex)
).toMutableList())) else
teleEntries.last().parameterNames.add(Pair(parameter.name, parameter.oldIndex))
val data = parameterToTeleWhitespaceData[parameter.oldIndex]
if (data != null && !usedWhitespaceData.contains(data)) {
usedWhitespaceData.add(data)
associatedWhitespaceData.add(Pair(teleEntries.last(), data))
}
}
val newTeles = StringBuilder()
for (entry in teleEntries) {
val whitespaceData = associatedWhitespaceData.firstOrNull { it.first == entry }?.second
newTeles.append(whitespaceData?.beforeTeleWhitespace ?: " ")
val parameterNames = StringBuilder()
for ((i, p) in entry.parameterNames.withIndex()) {
var space = parameterWhitespaceData[p.second] ?: " "
if (i == 0 && space.startsWith(" ")) space = space.drop(1)
if (i > 0 && space.isEmpty()) space = " "
parameterNames.append(space)
parameterNames.append(p.first.let{ if (it.isNullOrEmpty()) ArendElementTypes.UNDERSCORE else it })
}
val referableAllowsTypeTeles = locatedReferable is ArendConstructor || locatedReferable is ArendDefData
val printParameterNames = parameterNames.toString() != "_" || !referableAllowsTypeTeles
val printSurroundingParens = !entry.isExplicit || entry.typeText == null || printParameterNames
if (printSurroundingParens) newTeles.append (if (entry.isExplicit) ArendElementTypes.LPAREN else ArendElementTypes.LBRACE)
when (entry.accessModifier) {
AccessModifier.PRIVATE -> newTeles.append("${ArendElementTypes.PRIVATE_KW} ")
AccessModifier.PROTECTED -> newTeles.append("${ArendElementTypes.PROTECTED_KW} ")
else -> {}
}
if (entry.isCoerce) newTeles.append("${ArendElementTypes.COERCE_KW} ") else
if (entry.isClassifying) newTeles.append("${ArendElementTypes.CLASSIFYING_KW} ") else
if (entry.isProperty) newTeles.append("${ArendElementTypes.PROPERTY_KW} ")
if (entry.typeText != null) {
if (printParameterNames) {
newTeles.append(parameterNames.toString())
newTeles.append(whitespaceData?.colonText ?: " ${ArendElementTypes.COLON} ")
}
newTeles.append(if (entry.typeText.trim().contains(" ") && !printParameterNames && !printSurroundingParens) "(${entry.typeText})" else entry.typeText)
} else {
newTeles.append(parameterNames.toString())
}
newTeles.append(whitespaceData?.afterTypeText ?: "")
if (printSurroundingParens) newTeles.append (if (entry.isExplicit) ArendElementTypes.RPAREN else ArendElementTypes.RBRACE)
}
return newTeles.toString()
}