fun insertClauses()

in src/main/kotlin/org/arend/quickfix/ImplementMissingClausesQuickFix.kt [115:182]


        fun insertClauses(psiFactory: ArendPsiFactory, cause: ArendCompositeElement, clauses: List<ArendClause>) {
            var primerClause: ArendClause? = null// a "primer" clause which is needed only to simplify insertion of proper clauses

            val anchor = when (cause) {
                is ArendCoClauseDef -> {
                    val coClauseBody = cause.body
                            ?: (cause.addAfter(psiFactory.createCoClauseBody(), cause.lastChild) as ArendFunctionBody)
                    val elim = coClauseBody.elim
                            ?: coClauseBody.add(psiFactory.createCoClauseBody().descendantOfType<ArendElim>()!!)
                    if (coClauseBody.lbrace == null)
                        insertPairOfBraces(psiFactory, elim)

                    coClauseBody.clauseList.lastOrNull() ?: coClauseBody.lbrace ?: cause.lastChild
                }
                is ArendFunctionDefinition<*> -> {
                    val fBody = cause.body
                    val fClauses = if (fBody != null && fBody.kind != ArendFunctionBody.Kind.COCLAUSE) fBody.functionClauses else null

                    if (fBody != null) {
                        val lastChild = fBody.lastChild
                        if (fClauses != null) {
                            fClauses.clauseList.lastOrNull() ?: fClauses.lbrace ?: throw IllegalStateException()
                        } else {
                            val newClauses = psiFactory.createFunctionClauses()
                            val insertedClauses = lastChild.parent?.addAfter(newClauses, lastChild) as ArendFunctionClauses
                            lastChild.parent?.addAfter(psiFactory.createWhitespace(" "), lastChild)
                            primerClause = insertedClauses.lastChild as? ArendClause
                            primerClause
                        }
                    } else {
                        val newBody = psiFactory.createFunctionClauses().parent as ArendFunctionBody
                        val lastChild = cause.returnExpr ?: cause.parameters.lastOrNull() ?: throw IllegalStateException()
                        cause.addAfter(newBody, lastChild)
                        cause.addAfter(psiFactory.createWhitespace(" "), lastChild)
                        primerClause = cause.body?.functionClauses?.lastChild as? ArendClause
                        primerClause
                    }
                }
                is ArendCaseExpr -> {
                    val body = cause.withBody
                    val caseExprAnchor = cause.returnExpr ?: cause.caseArguments.lastOrNull()
                    body?.clauseList?.lastOrNull() ?: (body?.lbrace ?: (
                            body?.let {
                                insertPairOfBraces(psiFactory, it.withKw)
                                body.lbrace
                            } ?: (cause.addAfter(psiFactory.createWithBody(), caseExprAnchor) as ArendWithBody).lbrace))
                }
                is ArendLongName -> {
                    findWithBodyAnchor(cause.ancestor(), psiFactory)
                }
                is ArendWithBody -> findWithBodyAnchor(cause.parent as? ArendNewExpr, psiFactory)
                else -> null
            }
            val anchorParent = anchor?.parent
            for (clause in clauses) if (anchorParent != null) {
                val pipe = clause.findPrevSibling()
                var currAnchor: PsiElement? = null
                if (pipe != null) currAnchor = anchorParent.addAfter(pipe, anchor)
                anchorParent.addBefore(psiFactory.createWhitespace("\n"), currAnchor)
                currAnchor = anchorParent.addAfter(clause, currAnchor)
                anchorParent.addBefore(psiFactory.createWhitespace(" "), currAnchor)
            }

            primerClause?.let {
                it.findPrevSibling()?.delete()
                it.delete()
            }
        }