Skip to content

Commit

Permalink
Fix definition run configuration
Browse files Browse the repository at this point in the history
  • Loading branch information
alex999990009 committed Jun 25, 2024
1 parent f743b49 commit 783e712
Showing 6 changed files with 26 additions and 9 deletions.
22 changes: 14 additions & 8 deletions src/main/kotlin/org/arend/definition/ArendFileDefinitionScope.kt
Original file line number Diff line number Diff line change
@@ -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))
}
6 changes: 5 additions & 1 deletion src/main/kotlin/org/arend/resolving/ArendReference.kt
Original file line number Diff line number Diff line change
@@ -108,7 +108,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) {
2 changes: 2 additions & 0 deletions src/main/kotlin/org/arend/resolving/DataLocatedReferable.kt
Original file line number Diff line number Diff line change
@@ -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

2 changes: 2 additions & 0 deletions src/main/kotlin/org/arend/resolving/IntellijMetaReferable.kt
Original file line number Diff line number Diff line change
@@ -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()
}
Original file line number Diff line number Diff line change
@@ -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()
}
1 change: 1 addition & 0 deletions src/main/kotlin/org/arend/resolving/IntellijTCReferable.kt
Original file line number Diff line number Diff line change
@@ -6,4 +6,5 @@ import org.arend.naming.reference.TCReferable
interface IntellijTCReferable : TCReferable {
fun isEquivalent(ref: LocatedReferable): Boolean
val isConsistent: Boolean
var displayName: String?
}

0 comments on commit 783e712

Please sign in to comment.