From 67aeb20c21e46d76d1fff70fcdd9000eae65e0af Mon Sep 17 00:00:00 2001
From: "Aleksei.Luchinin" <alex999990009@gmail.com>
Date: Thu, 4 Jul 2024 15:12:32 +0300
Subject: [PATCH 1/3] Fix #525

---
 src/main/kotlin/org/arend/highlight/BasePass.kt | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/main/kotlin/org/arend/highlight/BasePass.kt b/src/main/kotlin/org/arend/highlight/BasePass.kt
index 2a9183383..d875017c7 100644
--- a/src/main/kotlin/org/arend/highlight/BasePass.kt
+++ b/src/main/kotlin/org/arend/highlight/BasePass.kt
@@ -118,7 +118,19 @@ abstract class BasePass(protected open val file: IArendFile, editor: Editor, nam
         return HighlightInfo.newHighlightInfo(type ?: levelToHighlightInfoType(error.level))
             .range(range)
             .severity(levelToSeverity(error.level))
-            .description(error.shortMessage)
+            .description(
+                run {
+                    var message: String? = null
+                    ApplicationManager.getApplication().run {
+                        executeOnPooledThread {
+                            runReadAction {
+                                message = error.shortMessage
+                            }
+                        }.get()
+                    }
+                    message ?: ""
+                }
+            )
             .escapedToolTip(XmlStringUtil.escapeString(DocStringBuilder.build(vHang(error.getShortHeaderDoc(ppConfig), error.getBodyDoc(ppConfig)))).replace("\n", "<br>"))
     }
 

From fcb2306361afbfc2d655e8b30a8174909a1cd83f Mon Sep 17 00:00:00 2001
From: "Aleksei.Luchinin" <alex999990009@gmail.com>
Date: Fri, 5 Jul 2024 13:15:45 +0300
Subject: [PATCH 2/3] Fix #527

---
 .../codeInsight/ArendLineMarkerProvider.kt    | 22 +++----------------
 1 file changed, 3 insertions(+), 19 deletions(-)

diff --git a/src/main/kotlin/org/arend/codeInsight/ArendLineMarkerProvider.kt b/src/main/kotlin/org/arend/codeInsight/ArendLineMarkerProvider.kt
index 59630f64c..9883a8068 100644
--- a/src/main/kotlin/org/arend/codeInsight/ArendLineMarkerProvider.kt
+++ b/src/main/kotlin/org/arend/codeInsight/ArendLineMarkerProvider.kt
@@ -5,19 +5,15 @@ import com.intellij.codeInsight.daemon.LineMarkerInfo
 import com.intellij.codeInsight.daemon.LineMarkerProviderDescriptor
 import com.intellij.codeInsight.daemon.impl.LineMarkerNavigator
 import com.intellij.codeInsight.daemon.impl.MarkerType
-import com.intellij.codeInsight.daemon.impl.PsiElementListNavigator
-import com.intellij.codeInsight.navigation.BackgroundUpdaterTask
+import com.intellij.codeInsight.navigation.PsiTargetNavigator
 import com.intellij.icons.AllIcons
-import com.intellij.ide.util.PsiElementListCellRenderer
 import com.intellij.openapi.components.service
 import com.intellij.openapi.editor.markup.GutterIconRenderer
 import com.intellij.openapi.progress.ProgressManager
 import com.intellij.psi.PsiElement
 import org.arend.psi.ext.ArendDefClass
 import org.arend.psi.ext.ArendDefIdentifier
-import org.arend.psi.ext.ArendDefinition
 import org.arend.search.ClassDescendantsSearch
-import org.arend.util.FullName
 import java.awt.event.MouseEvent
 
 class ArendLineMarkerProvider: LineMarkerProviderDescriptor() {
@@ -45,20 +41,8 @@ class ArendLineMarkerProvider: LineMarkerProviderDescriptor() {
             object : LineMarkerNavigator() {
                 override fun browse(e: MouseEvent, element: PsiElement) {
                     val clazz = element.parent.parent as? ArendDefClass ?: return
-                    PsiElementListNavigator.openTargets(e, clazz.project.service<ClassDescendantsSearch>().getAllDescendants(clazz).toTypedArray(), "Subclasses of " + clazz.name,
-                        CodeInsightBundle.message("goto.implementation.findUsages.title", clazz.refName), MyListCellRenderer, null as BackgroundUpdaterTask?)
+                    PsiTargetNavigator(clazz.project.service<ClassDescendantsSearch>().getAllDescendants(clazz).toTypedArray()).navigate(e, "Subclasses of " + clazz.name, element.project)
                 }
             })
     }
-
-    private object MyListCellRenderer : PsiElementListCellRenderer<ArendDefinition<*>>() {
-        override fun getElementText(element: ArendDefinition<*>): String {
-            val fullName = FullName(element)
-            return fullName.longName.toString() + " in " + fullName.modulePath.toString()
-        }
-
-        override fun getContainerText(element: ArendDefinition<*>, name: String): String? = null
-
-        override fun getIconFlags() = 0
-    }
-}
\ No newline at end of file
+}

From 271fee3eab58ba77f21d14d51e0c6a8bd35f79b5 Mon Sep 17 00:00:00 2001
From: "Aleksei.Luchinin" <alex999990009@gmail.com>
Date: Fri, 5 Jul 2024 13:40:13 +0300
Subject: [PATCH 3/3] Fix #526

---
 .../kotlin/org/arend/typechecking/error/ErrorService.kt   | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/main/kotlin/org/arend/typechecking/error/ErrorService.kt b/src/main/kotlin/org/arend/typechecking/error/ErrorService.kt
index d88d7f856..5f0ae752d 100644
--- a/src/main/kotlin/org/arend/typechecking/error/ErrorService.kt
+++ b/src/main/kotlin/org/arend/typechecking/error/ErrorService.kt
@@ -121,9 +121,11 @@ class ErrorService : ErrorReporter {
         val arendErrors = typecheckingErrors[file] ?: return emptyList()
 
         val list = ArrayList<Pair<GeneralError, PsiElement>>()
-        for (arendError in arendErrors) {
-            arendError.cause?.let {
-                list.add(Pair(arendError.error, it))
+        synchronized(arendErrors) {
+            for (arendError in arendErrors) {
+                arendError.cause?.let {
+                    list.add(Pair(arendError.error, it))
+                }
             }
         }
         return list