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