Merge pull request #522 from alex999990009/alex99999/fixes

Fix goto, run configuration and slow operations
JetBrains · Jun 26, 2024 · 5962aa1 · 5962aa1
2 parents 09f2b9e + 3833869
commit 5962aa1
Show file tree

Hide file tree

Showing 8 changed files with 36 additions and 12 deletions.
diff --git a/src/main/kotlin/org/arend/definition/ArendFileDefinitionScope.kt b/src/main/kotlin/org/arend/definition/ArendFileDefinitionScope.kt
@@ -1,28 +1,34 @@
 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<Referable> {
         val result = ArrayList<Referable>()
-        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)
+                    }
                 }
             }
         }
         return result
     }
 
     override fun getElements(kind: Referable.RefKind?): Collection<Referable> = 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/module/config/LibraryConfig.kt b/src/main/kotlin/org/arend/module/config/LibraryConfig.kt
@@ -201,15 +201,15 @@ 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
             }
         }
 
         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

diff --git a/src/main/kotlin/org/arend/resolving/ArendReference.kt b/src/main/kotlin/org/arend/resolving/ArendReference.kt
@@ -106,7 +106,11 @@ abstract class ArendReferenceBase<T : ArendReferenceElement>(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
@@ -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
@@ -21,4 +21,6 @@ class IntellijMetaReferable(private val underlyingRef: SmartPsiElementPointer<Ps
             val underlyingRef = underlyingRef?.element
             return underlyingRef != null && isEquivalent(underlyingRef)
         }
+
+    override var displayName: String? = refLongName.toString()
 }
diff --git a/src/main/kotlin/org/arend/resolving/IntellijTCLevelReferable.kt b/src/main/kotlin/org/arend/resolving/IntellijTCLevelReferable.kt
@@ -20,4 +20,6 @@ class IntellijTCLevelReferable(data: SmartPsiElementPointer<PsiLocatedReferable>
             val underlyingRef = runReadAction { data.element }
             return underlyingRef != null && isEquivalent(underlyingRef)
         }
+
+    override var displayName: String? = refLongName.toString()
 }
diff --git 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?
 }
diff --git 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<String>, 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