From 301a524117a59546bce055e9253ef40b0548d31e Mon Sep 17 00:00:00 2001 From: "Aleksei.Luchinin" Date: Mon, 17 Jun 2024 18:15:49 +0300 Subject: [PATCH 1/2] Fix #517 --- src/main/kotlin/org/arend/tracer/ArendSuspendContext.kt | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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()) } From e0b7c1e71674de41da877fba69b3d513b4e0bb23 Mon Sep 17 00:00:00 2001 From: "Aleksei.Luchinin" Date: Fri, 21 Jun 2024 15:18:35 +0300 Subject: [PATCH 2/2] Fix #365 --- .../org/arend/tracer/ArendTraceAction.kt | 24 ++++++++++++------- 1 file changed, 16 insertions(+), 8 deletions(-) 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