From f743b49ee03fd44480b41e3bf8a376b562252cc2 Mon Sep 17 00:00:00 2001 From: "Aleksei.Luchinin" Date: Tue, 25 Jun 2024 12:13:33 +0300 Subject: [PATCH 1/3] Fix GoTo File in \import --- src/main/kotlin/org/arend/module/config/LibraryConfig.kt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/kotlin/org/arend/module/config/LibraryConfig.kt b/src/main/kotlin/org/arend/module/config/LibraryConfig.kt index a87bb0648..8cf606bf7 100644 --- a/src/main/kotlin/org/arend/module/config/LibraryConfig.kt +++ b/src/main/kotlin/org/arend/module/config/LibraryConfig.kt @@ -201,7 +201,7 @@ abstract class LibraryConfig(val project: Project) { val psiManager = PsiManager.getInstance(project) val srcDir = findParentDirectory(modulePath, false) - findArendFileOrDirectoryByModulePath(srcDir, modulePath)?.let { + srcDir?.findChild(modulePath.lastName + EXTENSION)?.let { val file = psiManager.findFile(it) if (file is ArendFile) { return file @@ -209,7 +209,7 @@ abstract class LibraryConfig(val project: Project) { } val testDir = if (withTests) findParentDirectory(modulePath, true) else null - findArendFileOrDirectoryByModulePath(testDir, modulePath)?.let { + testDir?.findChild(modulePath.lastName + EXTENSION)?.let { val file = psiManager.findFile(it) if (file is ArendFile) { return file From 783e712bde740ca25067ec9f97dea375eb51879f Mon Sep 17 00:00:00 2001 From: "Aleksei.Luchinin" Date: Tue, 25 Jun 2024 19:40:28 +0300 Subject: [PATCH 2/3] Fix definition run configuration --- .../definition/ArendFileDefinitionScope.kt | 22 ++++++++++++------- .../org/arend/resolving/ArendReference.kt | 6 ++++- .../arend/resolving/DataLocatedReferable.kt | 2 ++ .../arend/resolving/IntellijMetaReferable.kt | 2 ++ .../resolving/IntellijTCLevelReferable.kt | 2 ++ .../arend/resolving/IntellijTCReferable.kt | 1 + 6 files changed, 26 insertions(+), 9 deletions(-) diff --git a/src/main/kotlin/org/arend/definition/ArendFileDefinitionScope.kt b/src/main/kotlin/org/arend/definition/ArendFileDefinitionScope.kt index a3f14d5f1..503abe797 100644 --- a/src/main/kotlin/org/arend/definition/ArendFileDefinitionScope.kt +++ b/src/main/kotlin/org/arend/definition/ArendFileDefinitionScope.kt @@ -1,23 +1,27 @@ package org.arend.definition import org.arend.error.DummyErrorReporter -import org.arend.naming.reference.LocatedReferable +import org.arend.ext.module.ModulePath +import org.arend.naming.reference.GlobalReferable import org.arend.naming.reference.Referable -import org.arend.naming.scope.LexicalScope import org.arend.naming.scope.Scope import org.arend.psi.ArendFile import org.arend.resolving.PsiConcreteProvider import org.arend.term.concrete.Concrete -class ArendFileDefinitionScope(private val arendFile: ArendFile) : Scope { +class ArendFileDefinitionScope(private val arendFile: ArendFile, private val extraPath: ModulePath = ModulePath()) : Scope { override fun getElements(): Collection { val result = ArrayList() - arendFile.apply { - val concreteProvider = PsiConcreteProvider(arendFile.project, DummyErrorReporter.INSTANCE, null) - LexicalScope.opened(this).elements.forEach { - val ref = concreteProvider.getConcrete(it as LocatedReferable) + val concreteProvider = PsiConcreteProvider(arendFile.project, DummyErrorReporter.INSTANCE, null) + arendFile.getTCRefMap(Referable.RefKind.EXPR).forEach { + if (ModulePath(it.key.toList().subList(0, extraPath.size())) == extraPath) { + val ref = concreteProvider.getConcrete(it.value as GlobalReferable) if (ref is Concrete.Definition) { - result.add(it) + val referable = it.value + referable.displayName = referable.refLongName.toString().removePrefix(extraPath.toString()).removePrefix(".") + if (referable.displayName!!.isNotEmpty()) { + result.add(referable) + } } } } @@ -25,4 +29,6 @@ class ArendFileDefinitionScope(private val arendFile: ArendFile) : Scope { } override fun getElements(kind: Referable.RefKind?): Collection = if (kind == null || kind == Referable.RefKind.EXPR) elements else emptyList() + + override fun resolveNamespace(name: String, onlyInternal: Boolean) = ArendFileDefinitionScope(arendFile, ModulePath(extraPath.toList() + name)) } diff --git a/src/main/kotlin/org/arend/resolving/ArendReference.kt b/src/main/kotlin/org/arend/resolving/ArendReference.kt index a9ad15284..275e7aee6 100644 --- a/src/main/kotlin/org/arend/resolving/ArendReference.kt +++ b/src/main/kotlin/org/arend/resolving/ArendReference.kt @@ -108,7 +108,11 @@ abstract class ArendReferenceBase(element: T, range: is PsiNamedElement -> { val alias = (ref as? ReferableBase<*>)?.alias?.aliasIdentifier?.id?.text val aliasString = if (alias == null) "" else " $alias" - val elementName = origElement.refName + val elementName = if (origElement is IntellijTCReferable) { + origElement.displayName + } else { + origElement.refName + } val lookupString = lookup ?: (elementName + aliasString) var builder = LookupElementBuilder.create(ref, lookupString).withIcon(ref.getIcon(0)) if (fullName) { diff --git a/src/main/kotlin/org/arend/resolving/DataLocatedReferable.kt b/src/main/kotlin/org/arend/resolving/DataLocatedReferable.kt index eee33ce61..8a9b188ad 100644 --- a/src/main/kotlin/org/arend/resolving/DataLocatedReferable.kt +++ b/src/main/kotlin/org/arend/resolving/DataLocatedReferable.kt @@ -59,6 +59,8 @@ open class DataLocatedReferable( return underlyingRef != null && isEquivalent(underlyingRef) } + override var displayName: String? = refLongName.toString() + override fun getUnderlyingReferable() = psiElementPointer?.let { runReadAction { it.element }?.underlyingReferable } ?: this diff --git a/src/main/kotlin/org/arend/resolving/IntellijMetaReferable.kt b/src/main/kotlin/org/arend/resolving/IntellijMetaReferable.kt index 80912936a..883343ef1 100644 --- a/src/main/kotlin/org/arend/resolving/IntellijMetaReferable.kt +++ b/src/main/kotlin/org/arend/resolving/IntellijMetaReferable.kt @@ -21,4 +21,6 @@ class IntellijMetaReferable(private val underlyingRef: SmartPsiElementPointer val underlyingRef = runReadAction { data.element } return underlyingRef != null && isEquivalent(underlyingRef) } + + override var displayName: String? = refLongName.toString() } \ No newline at end of file diff --git a/src/main/kotlin/org/arend/resolving/IntellijTCReferable.kt b/src/main/kotlin/org/arend/resolving/IntellijTCReferable.kt index bca9cae57..e26229608 100644 --- a/src/main/kotlin/org/arend/resolving/IntellijTCReferable.kt +++ b/src/main/kotlin/org/arend/resolving/IntellijTCReferable.kt @@ -6,4 +6,5 @@ import org.arend.naming.reference.TCReferable interface IntellijTCReferable : TCReferable { fun isEquivalent(ref: LocatedReferable): Boolean val isConsistent: Boolean + var displayName: String? } \ No newline at end of file From 3833869e4255431a0899b1f652032981da7850ec Mon Sep 17 00:00:00 2001 From: "Aleksei.Luchinin" Date: Tue, 25 Jun 2024 19:42:32 +0300 Subject: [PATCH 3/3] Fix SlowOperations --- src/main/kotlin/org/arend/util/VirtualFileUtils.kt | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/main/kotlin/org/arend/util/VirtualFileUtils.kt b/src/main/kotlin/org/arend/util/VirtualFileUtils.kt index 704a3003b..e13faf0be 100644 --- a/src/main/kotlin/org/arend/util/VirtualFileUtils.kt +++ b/src/main/kotlin/org/arend/util/VirtualFileUtils.kt @@ -1,5 +1,6 @@ package org.arend.util +import com.intellij.openapi.application.ApplicationManager import com.intellij.openapi.vfs.JarFileSystem import com.intellij.openapi.vfs.VfsUtil import com.intellij.openapi.vfs.VirtualFile @@ -42,7 +43,13 @@ fun VirtualFile.getRelativeFile(path: Collection, ext: String = "", crea val VirtualFile.configFile: VirtualFile? get() = when { - isDirectory -> findChild(FileUtils.LIBRARY_CONFIG_FILE) + isDirectory -> { + var configFile: VirtualFile? = null + ApplicationManager.getApplication().executeOnPooledThread { + configFile = findChild(FileUtils.LIBRARY_CONFIG_FILE) + }.get() + configFile + } name == FileUtils.LIBRARY_CONFIG_FILE -> this name.endsWith(FileUtils.ZIP_EXTENSION) -> JarFileSystem.getInstance().getJarRootForLocalFile(this)?.findChild(FileUtils.LIBRARY_CONFIG_FILE) else -> null