Skip to content

Commit

Permalink
Add dummy generatePreview implementations
Browse files Browse the repository at this point in the history
  • Loading branch information
sxhya committed Nov 12, 2024
1 parent 8a056cc commit 27cc1ba
Show file tree
Hide file tree
Showing 7 changed files with 24 additions and 1 deletion.
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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
}
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -44,12 +45,14 @@ class GenerateFunctionFromGoalIntention : AbstractGenerateFunctionIntention() {
return file.findElementAt(editor.caretModel.offset)?.parentOfType<ArendGoal>(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<ArendGoal>(false) ?: return null
val errorService = project.service<ErrorService>()
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)
Expand Down
Original file line number Diff line number Diff line change
@@ -1,12 +1,14 @@
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
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
Expand Down Expand Up @@ -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
}
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -30,4 +32,6 @@ class ReplaceWithNormalFormIntention : SelectionIntention<ArendExpr>(ArendExpr::
}
}
}

override fun generatePreview(project: Project, editor: Editor, file: PsiFile): IntentionPreviewInfo = IntentionPreviewInfo.EMPTY
}
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -84,6 +86,8 @@ class SplitAtomPatternIntention : SelfTargetingIntention<PsiElement>(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) }
}
Expand Down
2 changes: 2 additions & 0 deletions src/main/kotlin/org/arend/intention/WrapInGoalIntention.kt
Original file line number Diff line number Diff line change
@@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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(
Expand Down

0 comments on commit 27cc1ba

Please sign in to comment.