diff --git a/src/main/kotlin/org/arend/intention/ExtractExpressionToFunctionIntention.kt b/src/main/kotlin/org/arend/intention/ExtractExpressionToFunctionIntention.kt index 92d13d0f5..b15019301 100644 --- a/src/main/kotlin/org/arend/intention/ExtractExpressionToFunctionIntention.kt +++ b/src/main/kotlin/org/arend/intention/ExtractExpressionToFunctionIntention.kt @@ -1,5 +1,6 @@ package org.arend.intention +import com.intellij.codeInsight.intention.preview.IntentionPreviewInfo import com.intellij.openapi.editor.Editor import com.intellij.openapi.project.Project import com.intellij.psi.PsiFile @@ -50,4 +51,6 @@ open class ExtractExpressionToFunctionIntention : AbstractGenerateFunctionIntent } override fun extractSelectionData(file: PsiFile, editor: Editor, project: Project): SelectionResult? = doExtractSelectionData(file, editor, project) + + override fun generatePreview(project: Project, editor: Editor, file: PsiFile): IntentionPreviewInfo = IntentionPreviewInfo.EMPTY } \ No newline at end of file diff --git a/src/main/kotlin/org/arend/intention/GenerateFunctionFromGoalIntention.kt b/src/main/kotlin/org/arend/intention/GenerateFunctionFromGoalIntention.kt index 6c6e3d030..cd6cf1426 100644 --- a/src/main/kotlin/org/arend/intention/GenerateFunctionFromGoalIntention.kt +++ b/src/main/kotlin/org/arend/intention/GenerateFunctionFromGoalIntention.kt @@ -1,5 +1,6 @@ package org.arend.intention +import com.intellij.codeInsight.intention.preview.IntentionPreviewInfo import com.intellij.openapi.components.service import com.intellij.openapi.editor.Editor import com.intellij.openapi.project.Project @@ -44,12 +45,14 @@ class GenerateFunctionFromGoalIntention : AbstractGenerateFunctionIntention() { return file.findElementAt(editor.caretModel.offset)?.parentOfType(false) != null } + override fun generatePreview(project: Project, editor: Editor, file: PsiFile): IntentionPreviewInfo = IntentionPreviewInfo.EMPTY + override fun extractSelectionData(file: PsiFile, editor: Editor, project: Project): SelectionResult? { val goal = file.findElementAt(editor.caretModel.offset)?.parentOfType(false) ?: return null val errorService = project.service() val arendError = errorService.errors[goal.containingFile]?.firstOrNull { it.cause == goal }?.error as? GoalError ?: return null - val goalType = (arendError as? GoalError)?.expectedType + val goalType = arendError.expectedType val (modifiedType, customArguments) = getCustomArguments(goal, goalType) { tryCorrespondedSubExpr(it, file, project, editor)?.subCore } val goalExpr = goal.expr?.let { tryCorrespondedSubExpr(it.textRange, file, project, editor) diff --git a/src/main/kotlin/org/arend/intention/ReplaceMetaWithResultIntention.kt b/src/main/kotlin/org/arend/intention/ReplaceMetaWithResultIntention.kt index 20ba5b0fb..63e4197cc 100644 --- a/src/main/kotlin/org/arend/intention/ReplaceMetaWithResultIntention.kt +++ b/src/main/kotlin/org/arend/intention/ReplaceMetaWithResultIntention.kt @@ -1,5 +1,6 @@ package org.arend.intention +import com.intellij.codeInsight.intention.preview.IntentionPreviewInfo import com.intellij.openapi.application.ApplicationManager import com.intellij.openapi.application.runReadAction import com.intellij.openapi.command.WriteCommandAction @@ -7,6 +8,7 @@ import com.intellij.openapi.editor.Editor import com.intellij.openapi.project.Project import com.intellij.psi.PsiDocumentManager import com.intellij.psi.PsiElement +import com.intellij.psi.PsiFile import org.arend.core.expr.ErrorWithConcreteExpression import org.arend.extImpl.definitionRenamer.CachingDefinitionRenamer import org.arend.psi.ArendFile @@ -45,4 +47,6 @@ class ReplaceMetaWithResultIntention : BaseArendIntention(ArendBundle.message("a replaceExprSmart(editor.document, expr, subConcrete, rangeOfConcrete(subConcrete), null, cExpr, text) } } + + override fun generatePreview(project: Project, editor: Editor, file: PsiFile): IntentionPreviewInfo = IntentionPreviewInfo.EMPTY } \ No newline at end of file diff --git a/src/main/kotlin/org/arend/intention/ReplaceWithNormalFormIntention.kt b/src/main/kotlin/org/arend/intention/ReplaceWithNormalFormIntention.kt index 6d43ec140..a1b92b244 100644 --- a/src/main/kotlin/org/arend/intention/ReplaceWithNormalFormIntention.kt +++ b/src/main/kotlin/org/arend/intention/ReplaceWithNormalFormIntention.kt @@ -1,9 +1,11 @@ package org.arend.intention +import com.intellij.codeInsight.intention.preview.IntentionPreviewInfo import com.intellij.openapi.command.WriteCommandAction import com.intellij.openapi.editor.Editor import com.intellij.openapi.project.Project import com.intellij.openapi.util.TextRange +import com.intellij.psi.PsiFile import org.arend.ext.core.ops.NormalizationMode import org.arend.extImpl.definitionRenamer.CachingDefinitionRenamer import org.arend.psi.ext.ArendExpr @@ -30,4 +32,6 @@ class ReplaceWithNormalFormIntention : SelectionIntention(ArendExpr:: } } } + + override fun generatePreview(project: Project, editor: Editor, file: PsiFile): IntentionPreviewInfo = IntentionPreviewInfo.EMPTY } \ No newline at end of file diff --git a/src/main/kotlin/org/arend/intention/SplitAtomPatternIntention.kt b/src/main/kotlin/org/arend/intention/SplitAtomPatternIntention.kt index b25d3ddaf..1baa95a29 100644 --- a/src/main/kotlin/org/arend/intention/SplitAtomPatternIntention.kt +++ b/src/main/kotlin/org/arend/intention/SplitAtomPatternIntention.kt @@ -1,8 +1,10 @@ package org.arend.intention +import com.intellij.codeInsight.intention.preview.IntentionPreviewInfo import com.intellij.openapi.editor.Editor import com.intellij.openapi.project.Project import com.intellij.psi.PsiElement +import com.intellij.psi.PsiFile import com.intellij.psi.util.startOffset import com.intellij.util.containers.tail import org.arend.ext.variable.Variable @@ -84,6 +86,8 @@ class SplitAtomPatternIntention : SelfTargetingIntention(PsiElement: return this.splitPatternEntries != null } + override fun generatePreview(project: Project, editor: Editor, file: PsiFile): IntentionPreviewInfo = IntentionPreviewInfo.EMPTY + override fun applyTo(element: PsiElement, project: Project, editor: Editor) { splitPatternEntries?.let { doSplitPattern(element, project, it) } } diff --git a/src/main/kotlin/org/arend/intention/WrapInGoalIntention.kt b/src/main/kotlin/org/arend/intention/WrapInGoalIntention.kt index 3ef827544..c45b7516b 100644 --- a/src/main/kotlin/org/arend/intention/WrapInGoalIntention.kt +++ b/src/main/kotlin/org/arend/intention/WrapInGoalIntention.kt @@ -1,8 +1,10 @@ package org.arend.intention +import com.intellij.codeInsight.intention.preview.IntentionPreviewInfo import com.intellij.openapi.editor.Editor import com.intellij.openapi.project.Project import com.intellij.openapi.util.TextRange +import com.intellij.psi.PsiFile import org.arend.psi.ext.ArendExpr import org.arend.psi.ArendFile import org.arend.psi.ext.ArendLiteral diff --git a/src/main/kotlin/org/arend/intention/generating/CreateLetBindingIntention.kt b/src/main/kotlin/org/arend/intention/generating/CreateLetBindingIntention.kt index 3c29172f0..1189fb6b0 100644 --- a/src/main/kotlin/org/arend/intention/generating/CreateLetBindingIntention.kt +++ b/src/main/kotlin/org/arend/intention/generating/CreateLetBindingIntention.kt @@ -3,6 +3,7 @@ package org.arend.intention.generating import com.intellij.codeInsight.daemon.DaemonCodeAnalyzer +import com.intellij.codeInsight.intention.preview.IntentionPreviewInfo import com.intellij.openapi.application.runWriteAction import com.intellij.openapi.command.CommandProcessor import com.intellij.openapi.command.executeCommand @@ -67,6 +68,8 @@ class CreateLetBindingIntention : AbstractGenerateFunctionIntention() { return collectWrappableOptions(subPsi, rangeOfConcrete(subConcrete)).isNotEmpty() } + override fun generatePreview(project: Project, editor: Editor, file: PsiFile): IntentionPreviewInfo = IntentionPreviewInfo.EMPTY + override fun getText(): String = ArendBundle.message("arend.create.let.binding") private data class WrappableOption(