search

JetBrains / intellij-arend

Arend plugin for IntelliJ IDEA
Apache License 2.0
90 stars 12 forks source link

Add non-dummy implementations for generatePreview #573

Open sxhya opened 3 days ago

sxhya commented 3 days ago

The following intention actions have dummy implementation for generatePreview.

ExtractExpressionToFunctionIntention
GenerateFunctionFromGoalIntention
ReplaceMetaWithResultIntention
ReplaceWithNormalFormIntention
SplitAtomPatternIntention
WrapInGoalIntention

The default generatePreview would not work for these functions since they all depend on tryCorrespondedSubExpr which creates effects (invokeLater). Get rid of effecs in tryCorrespondedSubExpr (remove invocations of HintAction.showError in preview code?). Check that previews actually work for these intentions.