fun updateEditors()

in src/main/kotlin/org/arend/toolWindow/errors/ArendMessagesView.kt [173:237]


    fun updateEditors() {
        val treeElement = getSelectedMessage()
        if (treeElement != null) {
            if (isGoal(treeElement) && !isGoalTextPinned()) {
                if (goalEditor == null) {
                    goalEditor = ArendMessagesViewEditor(project, treeElement, true)
                }
                if (!isImplicitGoal(treeElement) || isShowImplicitGoals()) {
                    updateEditor(goalEditor!!, treeElement)
                } else {
                    removeNotActionToolbars(goalEditor!!)
                }
                updateActionGroup(goalEditor!!)
                updateGoalsView(goalEditor?.component ?: goalEmptyPanel)
            }
            if (isShowErrorsPanel() && !isErrorTextPinned() && (!isGoal(treeElement) || isShowGoalsInErrorsPanel())) {
                if (errorEditor == null) {
                    errorEditor = ArendMessagesViewEditor(project, treeElement, false)
                }
                updateEditor(errorEditor!!, treeElement)
                updatePanel(errorsPanel, errorEditor?.component ?: errorEmptyPanel)
            }
            if (errorEditor?.isEmptyActionGroup() == true) {
                errorEditor?.setupActions()
            }
        } else {
            ApplicationManager.getApplication().executeOnPooledThread {
                runReadAction {
                    if (!isGoalTextPinned()) {
                        goalEditor?.treeElement?.sampleError?.let { currentGoal ->
                            if (isParentDefinitionPsiInvalid(currentGoal)) {
                                goalEditor?.clear()
                                updateGoalsView(goalEmptyPanel)
                            } else if (currentGoal.file?.isBackgroundTypecheckingFinished == true) {
                                val error = currentGoal.error
                                val (resolve, scope) = InjectedArendEditor.resolveCauseReference(error)
                                val doc = goalEditor?.treeElement?.let { goalEditor?.getDoc(it, error, resolve, scope) }

                                if (isParentDefinitionRemovedFromTree(currentGoal)) {
                                    goalEditor?.clear()
                                    updateGoalsView(goalEmptyPanel)
                                } else if (isCausePsiInvalid(currentGoal) && goalsTabInfo.text == defaultGoalsTabTitle) {
                                    runInEdt {
                                        goalsTabInfo.append(
                                            " (${ArendBundle.message("arend.messages.view.latest.goal.removed.title")})",
                                            SimpleTextAttributes.REGULAR_BOLD_ATTRIBUTES
                                        )
                                    }
                                } else if (goalEditor?.currentDoc.toString() != doc.toString()) {
                                    updateGoalText()
                                }
                            }
                        }
                    }
                    if (isShowErrorsPanel() && !isErrorTextPinned()) {
                        val currentError = errorEditor?.treeElement?.sampleError
                        if (currentError != null && isParentDefinitionRemovedFromTree(currentError)) {
                            errorEditor?.clear()
                            updatePanel(errorsPanel, errorEmptyPanel)
                        }
                    }
                }
            }
        }
    }