diff --git a/src/main/kotlin/org/arend/intention/generating/GenerateElimMissingClausesIntention.kt b/src/main/kotlin/org/arend/intention/generating/GenerateElimMissingClausesIntention.kt index 91916dd96..5052d3721 100644 --- a/src/main/kotlin/org/arend/intention/generating/GenerateElimMissingClausesIntention.kt +++ b/src/main/kotlin/org/arend/intention/generating/GenerateElimMissingClausesIntention.kt @@ -9,7 +9,7 @@ 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 @@ -17,7 +17,7 @@ import org.arend.util.ArendBundle class GenerateElimMissingClausesIntention : SelfTargetingIntention(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 index d453d928b..83fb4d32d 100644 --- 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::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 index 059e4db2a..5bf9e1fcb 100644 --- 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() - 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? {