Merge pull request #548 from alex999990009/alex99999/fixes

Fix comments and resolving long names

src/main/kotlin/org/arend/commenter/ArendCommenter.kt

@@ -8,7 +8,7 @@ import org.arend.psi.ArendElementTypes
 import org.arend.psi.doc.ArendDocComment
 
 class ArendCommenter : CodeDocumentationAwareCommenter {
-    override fun getLineCommentPrefix(): String = "--"
+    override fun getLineCommentPrefix(): String = "-- "
 
     override fun getBlockCommentPrefix(): String = "{-"
 

src/main/kotlin/org/arend/highlight/ArendHighlightingPass.kt

@@ -79,7 +79,7 @@ class ArendHighlightingPass(file: IArendFile, editor: Editor, textRange: TextRan
             }
         }
 
-        val resolveListener = object : ArendResolverListener(myProject.service()) {
+        val resolveListener = object : ArendResolverListener(myProject.service<ArendResolveCache>()) {
             override fun resolveReference(data: Any?, referent: Referable?, list: List<ArendReferenceElement>, resolvedRefs: List<Referable?>) {
                 val lastReference = list.lastOrNull() ?: return
                 if (data !is ArendPattern && (lastReference is ArendRefIdentifier || lastReference is ArendDefIdentifier)) {

src/main/kotlin/org/arend/injection/actions/NormalizationCache.kt

@@ -2,9 +2,10 @@ package org.arend.injection.actions
 
 import org.arend.core.expr.Expression
 import org.arend.ext.core.ops.NormalizationMode
+import java.util.concurrent.ConcurrentHashMap
 
 class NormalizationCache {
-    private val innerCache: MutableMap<Expression, Expression> = mutableMapOf()
+    private val innerCache = ConcurrentHashMap<Expression, Expression>()
 
     fun getNormalizedExpression(expr: Expression) : Expression {
         return if (innerCache.values.any { expr === it}) expr // referential equality is IMPORTANT. equals considers terms to be equal up to normal form. Here we explicitly distinguish nf and non-nf

src/main/kotlin/org/arend/psi/ArendFile.kt

@@ -7,6 +7,7 @@ import com.intellij.openapi.roots.LibraryOrderEntry
 import com.intellij.openapi.roots.ProjectFileIndex
 import com.intellij.psi.FileViewProvider
 import com.intellij.psi.PsiElement
+import com.intellij.psi.PsiReference
 import com.intellij.psi.impl.source.resolve.FileContextUtil
 import com.intellij.psi.util.CachedValueProvider
 import com.intellij.psi.util.CachedValuesManager
@@ -221,4 +222,11 @@ class ArendFile(viewProvider: FileViewProvider) : PsiFileBase(viewProvider, Aren
     override fun getParentSourceNode(): ArendSourceNode? = null
 
     override fun getIcon(flags: Int) = ArendIcons.AREND_FILE
+
+    override fun findReferenceAt(offset: Int): PsiReference? {
+        super.findReferenceAt(offset)?.let {
+            return it
+        }
+        return super.findReferenceAt(offset - 1)
+    }
 }

src/main/kotlin/org/arend/resolving/ArendReference.kt

@@ -70,7 +70,7 @@ abstract class ArendReferenceBase<T : ArendReferenceElement>(element: T, range:
                     }
                     expr != null -> {
                         ConcreteBuilder.convertExpression(expr).accept(ExpressionResolveNameVisitor(ArendReferableConverter, CachingScope.make(element.scope), ArrayList<Referable>(), DummyErrorReporter.INSTANCE, ArendResolverListener(cache)), null)
-                        cache.getCached(element)
+                        cache.getCached(element) ?: element.scope.resolveName(element.referenceName, refKind)
                     }
                     else -> element.scope.resolveName(element.referenceName, refKind)
                 }

src/main/kotlin/org/arend/resolving/ArendResolveCache.kt

@@ -6,35 +6,40 @@ import com.intellij.psi.PsiElement
 import com.intellij.psi.SmartPointerManager
 import com.intellij.psi.SmartPsiElementPointer
 import com.intellij.util.containers.ContainerUtil
+import okio.withLock
 import org.arend.naming.reference.Referable
-import org.arend.naming.reference.TCDefReferable
 import org.arend.psi.ext.ArendReferenceElement
 import org.arend.typechecking.TypeCheckingService
 import java.util.concurrent.ConcurrentMap
+import java.util.concurrent.locks.ReentrantLock
 
 class ArendResolveCache(project: Project) {
     private val typeCheckingService = project.service<TypeCheckingService>()
     private val refMap: ConcurrentMap<ArendReferenceElement, Referable> = ContainerUtil.createConcurrentWeakKeySoftValueMap()
     private val refMapPsi: ConcurrentMap<ArendReferenceElement, Pair<Int, SmartPsiElementPointer<PsiElement>>> = ContainerUtil.createConcurrentWeakMap()
 
+    private val lock = ReentrantLock()
+
     fun getCached(reference: ArendReferenceElement): Referable? {
-        val ref = refMap[reference]
-        if (ref != null/* && ref != TCDefReferable.NULL_REFERABLE*/) return ref
+        lock.withLock {
+            val ref = refMap[reference]
+            if (ref != null/* && ref != TCDefReferable.NULL_REFERABLE*/) return ref
 
-        val entry = refMapPsi[reference]
-        val psi = entry?.second?.element
-        val code = entry?.first
+            val entry = refMapPsi[reference]
+            val psi = entry?.second?.element
+            val code = entry?.first
 
-        if (code != null && code != reference.text.hashCode() || psi != null && !psi.isValid) { // Cached value is probably incorrect/broken
-            dropCache(reference)
-            return null
-        }
+            if (code != null && code != reference.text.hashCode() || psi != null && !psi.isValid) { // Cached value is probably incorrect/broken
+                dropCache(reference)
+                return null
+            }
 
-        if (psi is Referable) {
-            return psi
-        }
+            if (psi is Referable) {
+                return psi
+            }
 
-        return null
+            return null
+        }
     }
 
     fun resolveCached(resolver: () -> Referable?, reference: ArendReferenceElement): Referable? {
@@ -59,20 +64,26 @@ class ArendResolveCache(project: Project) {
 
     private fun doReplaceCache(newRef: Referable?, reference: ArendReferenceElement) {
         if (newRef is PsiElement && newRef.isValid) {
-            refMapPsi[reference] = Pair(reference.text.hashCode(), SmartPointerManager.createPointer(newRef))
-            refMap.remove(reference)
-        } else {
-            refMap[reference] = newRef ?: TCDefReferable.NULL_REFERABLE
+            lock.withLock {
+                refMapPsi[reference] = Pair(reference.text.hashCode(), SmartPointerManager.createPointer(newRef))
+                refMap.remove(reference)
+            }
+        } else if (newRef != null) {
+            refMap[reference] = newRef
         }
     }
 
     fun dropCache(reference: ArendReferenceElement) {
-        refMap.remove(reference)
-        refMapPsi.remove(reference)
+        lock.withLock {
+            refMap.remove(reference)
+            refMapPsi.remove(reference)
+        }
     }
 
     fun clear() {
-        refMap.clear()
-        refMapPsi.clear()
+        lock.withLock {
+            refMap.clear()
+            refMapPsi.clear()
+        }
     }
-}
+}

src/test/resources/org/arend/commenter/fixtures/indented_single_line_comment_after.ard

@@ -1,3 +1,3 @@
 \data Nat
---    | zero
-    | s<caret>uc Nat
+--     | zero
+    | su<caret>c Nat

src/test/resources/org/arend/commenter/fixtures/multi_line_after.ard

@@ -1,3 +1,3 @@
---\data <selection>Nat
---    |</selection> zero
+-- \data <selection>Nat
+--     |</selection> zero
     | suc Nat

src/test/resources/org/arend/commenter/fixtures/multi_line_uncomment.ard

@@ -1,3 +1,3 @@
---\data <selection>Nat
---    |</selection> zero
+-- \data <selection>Nat
+--     |</selection> zero
     | suc Nat

src/test/resources/org/arend/commenter/fixtures/single_line_after.ard

@@ -1,3 +1,3 @@
---\data Nat
-    |zer<caret>o
+-- \data Nat
+    |zero<caret>
     | suc Nat

src/test/resources/org/arend/commenter/fixtures/single_line_uncomment.ard

@@ -1,3 +1,3 @@
---\data <caret>Nat
+-- \data <caret>Nat
     |zero
     | suc Nat

src/test/resources/org/arend/commenter/fixtures/single_line_uncomment_with_space.ard

@@ -1,3 +1,3 @@
--- \data <caret>Nat
+--  \data <caret>Nat
     |zero
     | suc Nat