Fix GenerateMissingClauses

JetBrains · Sep 13, 2024 · f279061 · f279061
1 parent 5bbae1d
commit f279061
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 35 deletions.
diff --git a/src/main/kotlin/org/arend/intention/generating/GenerateElimMissingClausesIntention.kt b/src/main/kotlin/org/arend/intention/generating/GenerateElimMissingClausesIntention.kt
@@ -9,15 +9,15 @@ import com.intellij.openapi.application.runWriteAction
 import com.intellij.openapi.editor.Editor
 import com.intellij.openapi.project.Project
 import com.intellij.psi.PsiElement
-import com.intellij.refactoring.suggested.endOffset
+import com.intellij.psi.util.endOffset
 import org.arend.intention.SelfTargetingIntention
 import org.arend.psi.ArendFile
 import org.arend.psi.ArendPsiFactory
 import org.arend.util.ArendBundle
 
 class GenerateElimMissingClausesIntention : SelfTargetingIntention<PsiElement>(PsiElement::class.java, ArendBundle.message("arend.generateElimPatternMatchingClauses")) {
     override fun isApplicableTo(element: PsiElement, caretOffset: Int, editor: Editor): Boolean {
-        return checkMissingClauses(element, editor)
+        return checkMissingClauses(element)
     }
 
     override fun applyTo(element: PsiElement, project: Project, editor: Editor) {

diff --git a/src/main/kotlin/org/arend/intention/generating/GenerateMissingClausesIntention.kt b/src/main/kotlin/org/arend/intention/generating/GenerateMissingClausesIntention.kt
@@ -9,7 +9,7 @@ import org.arend.util.ArendBundle
 
 class GenerateMissingClausesIntention : SelfTargetingIntention<PsiElement>(PsiElement::class.java, ArendBundle.message("arend.generatePatternMatchingClauses")) {
     override fun isApplicableTo(element: PsiElement, caretOffset: Int, editor: Editor): Boolean {
-        return checkMissingClauses(element, editor)
+        return checkMissingClauses(element)
     }
 
     override fun applyTo(element: PsiElement, project: Project, editor: Editor) {

diff --git a/src/main/kotlin/org/arend/intention/generating/GenerateMissingClausesUtils.kt b/src/main/kotlin/org/arend/intention/generating/GenerateMissingClausesUtils.kt
@@ -7,46 +7,18 @@ import com.intellij.openapi.project.Project
 import com.intellij.psi.PsiElement
 import com.intellij.psi.SmartPointerManager
 import com.intellij.psi.util.elementType
-import com.intellij.refactoring.suggested.endOffset
-import com.intellij.refactoring.suggested.startOffset
+import com.intellij.psi.util.endOffset
+import com.intellij.psi.util.startOffset
 import org.arend.ext.error.MissingClausesError
 import org.arend.psi.ArendElementTypes
 import org.arend.psi.ArendFile
-import org.arend.psi.ArendPsiFactory
 import org.arend.psi.ext.*
 import org.arend.quickfix.ImplementMissingClausesQuickFix
 import org.arend.typechecking.ArendTypechecking
 import org.arend.typechecking.error.ErrorService
 
-internal fun checkMissingClauses(element: PsiElement, editor: Editor): Boolean {
-    if (element.elementType != ArendElementTypes.TGOAL) {
-        return false
-    }
-    var fileText = (element.containingFile as ArendFile).text
-
-    var parent: PsiElement? = element
-    while (parent !is ArendFunctionBody) {
-        parent = parent?.parent
-        if (parent == null) {
-            return false
-        }
-    }
-    fileText = fileText.removeRange(parent.startOffset, parent.endOffset)
-
-    val project = editor.project ?: return false
-    val psiFactory = ArendPsiFactory(project)
-    val newFile = psiFactory.createFromText(fileText) ?: return false
-
-    ArendTypechecking.create(project).typecheckModules(listOf(newFile), null)
-
-    val errorService = project.service<ErrorService>()
-    val error = errorService.getErrors(newFile).filter { it.error is MissingClausesError }.find {
-        it.definition?.endOffset?.plus(1) == parent.startOffset
-    }
-
-    errorService.clearNameResolverErrors(newFile)
-    errorService.clearTypecheckingErrors(newFile)
-    return error != null
+internal fun checkMissingClauses(element: PsiElement): Boolean {
+    return element.elementType == ArendElementTypes.TGOAL
 }
 
 internal fun deleteFunctionBody(element: PsiElement): Pair<ArendGroup, Int>? {