Merge pull request #521 from alex999990009/alex99999/fixes

Fix tracer
JetBrains · Jun 21, 2024 · 09f2b9e · 09f2b9e
2 parents 6ff0213 + e0b7c1e
commit 09f2b9e
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 9 deletions.
diff --git a/src/main/kotlin/org/arend/tracer/ArendSuspendContext.kt b/src/main/kotlin/org/arend/tracer/ArendSuspendContext.kt
@@ -70,7 +70,9 @@ class ArendSuspendContext(traceEntry: ArendTraceEntry, contextView: ArendTraceCo
                 }
             }
             val psiElement = getSourcePositionElement(traceEntry)
-            val psiText = psiElement?.text?.let(::shorten) ?: ArendBundle.message("arend.tracer.unknown.expression")
+            val psiText = runReadAction {
+                psiElement?.text?.let(::shorten) ?: ArendBundle.message("arend.tracer.unknown.expression")
+            }
             component.append(psiText, SimpleTextAttributes.REGULAR_ATTRIBUTES)
             setPositionText(component, positionComponents())
         }

diff --git a/src/main/kotlin/org/arend/tracer/ArendTraceAction.kt b/src/main/kotlin/org/arend/tracer/ArendTraceAction.kt
@@ -123,16 +123,24 @@ class ArendTraceAction : ArendPopupAction() {
                 is ArendDefData -> {
                     val body = def.dataBody ?: return null
                     val constructors = body.constructorList
-                    val constructor = constructors.firstOrNull()
-                        ?: body.constructorClauseList.find { it.constructors.isNotEmpty() }?.constructors?.firstOrNull()
-                    constructor?.parameters?.firstOrNull()?.typedExpr?.type
+                    val constructor = constructors.find {
+                        it.parameters.isNotEmpty()
+                    } ?: body.constructorClauseList.find {
+                            it.constructors.any { constructor -> constructor.parameters.isNotEmpty() }
+                        }?.constructors?.find {
+                            it.parameters.isNotEmpty()
+                        }
+                    constructor?.parameters?.firstOrNull()?.type
                 }
                 is ArendDefClass -> {
-                    val classStat = def.classStatList.firstOrNull() ?: return null
-                    classStat.classField?.returnExpr?.type
-                        ?: classStat.classImplement?.expr
-                        ?: classStat.coClause?.expr
-                        ?: classStat.overriddenField?.returnExpr?.type
+                    val classStat = def.classStatList.firstOrNull()
+                    classStat?.classField?.returnExpr?.type
+                        ?: classStat?.classImplement?.expr?.type
+                        ?: classStat?.coClause?.expr?.type
+                        ?: classStat?.overriddenField?.returnExpr?.type
+                        ?: def.classFieldList.firstOrNull()?.returnExpr?.type
+                        ?: def.classImplementList.firstOrNull()?.expr?.type
+                        ?: def.fieldTeleList.firstOrNull()?.type
                 }
                 else -> return null
             } ?: return null