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