Merge pull request #530 from alex999990009/alex99999/fixes

Fix exceptions
JetBrains · Jul 5, 2024 · de83e98 · de83e98
2 parents 44a2023 + 271fee3
commit de83e98
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 23 deletions.
diff --git 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
-    }
-}
+}
diff --git 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>"))
     }
 

diff --git 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