fun selectErrorFromEditor()

in src/main/kotlin/org/arend/actions/ArendGotoNextErrorAction.kt [40:82]


fun selectErrorFromEditor(project: Project, editor: Editor, file: ArendFile?, always: Boolean, activate: Boolean) {
    val document = editor.document
    val offset = editor.caretModel.offset
    // Check that we are in a problem range
    if ((DocumentMarkupModel.forDocument(document, project, true) as? MarkupModelEx)?.processRangeHighlightersOverlappingWith(offset, offset + 1, CommonProcessors.alwaysFalse()) == true) {
        return
    }

    ApplicationManager.getApplication().run {
        executeOnPooledThread {
            var arendFile = file
            if (arendFile == null) {
                runReadAction {
                    arendFile = PsiDocumentManager.getInstance(project).getPsiFile(document) as? ArendFile
                }
            }
            if (arendFile == null) {
                return@executeOnPooledThread
            }
            runInEdt {
                val arendErrors = project.service<ErrorService>().getErrors(arendFile!!)
                if (arendErrors.isEmpty()) {
                    return@runInEdt
                }

                val service = project.service<ArendProjectSettings>()
                for (arendError in arendErrors) {
                    if (always || arendError.error.satisfies(service.autoScrollFromSource)) {
                        val textRange = BasePass.getImprovedTextRange(arendError.error) ?: continue
                        if (textRange.containsOffset(offset)) {
                            val messagesService = project.service<ArendMessagesService>()
                            messagesService.view?.tree?.select(arendError.error)
                            if (activate) {
                                messagesService.activate(project, false)
                            }
                            break
                        }
                    }
                }
            }
        }
    }
}