diff --git a/src/main/kotlin/org/arend/tracer/ArendSuspendContext.kt b/src/main/kotlin/org/arend/tracer/ArendSuspendContext.kt index 078fbedb0..e27a7b17e 100644 --- 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 index 997f5b8ad..24ce47ebc 100644 --- a/src/main/kotlin/org/arend/tracer/ArendTraceAction.kt +++ b/src/main/kotlin/org/arend/tracer/ArendTraceAction.kt @@ -122,16 +122,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