intellij-arend
intellij-arend copied to clipboard
JetBrains
Arend plugin for IntelliJ IDEA
Implicit arguments can be substituted with `?x`, where `x` is the name of the argument. Also, if the expression is type-checked, then the argument can be substituted with the inferred...
The signature of \use \level definitions is non-trivial, but it can be generated completely automatically.
This behavior should be configurable.
Extend the https://github.com/JetBrains/intellij-community/blob/master/platform/core-api/src/com/intellij/psi/PsiBinaryFile.java interface
Maybe we should internationalize intellij-arend. Doc: https://www.jetbrains.org/intellij/sdk/docs/reference_guide/localization_guide.html
We need to profile and fix this performance issue.
``` java.lang.Throwable: 'psi.File' is requested on EDT by SmartSelect#update@keyboard shortcut (com.intellij.ide.actions.SmartSelect). See ActionUpdateThread javadoc. at com.intellij.openapi.diagnostic.Logger.error(Logger.java:202) at com.intellij.openapi.actionSystem.impl.PreCachedDataContext.reportValueProvidedByRulesUsage(PreCachedDataContext.java:245) at com.intellij.openapi.actionSystem.impl.PreCachedDataContext.getDataInner(PreCachedDataContext.java:209) at com.intellij.openapi.actionSystem.impl.PreCachedDataContext.getData(PreCachedDataContext.java:162) at org.arend.actions.ArendSmartSelectProvider.getSource(ArendSmartSelectProvider.kt:80) at org.arend.actions.ArendSmartSelectProvider.getSource(ArendSmartSelectProvider.kt:19) at com.intellij.openapi.ide.SmartSelectProvider.isEnabled(SmartSelectProvider.java:33) at com.intellij.ide.actions.SmartSelect.getProvider(SmartSelect.java:63)...
``` java.lang.NullPointerException at org.arend.intention.SplitAtomPatternIntention.getElementType(SplitAtomPatternIntention.kt:161) at org.arend.intention.SplitAtomPatternIntention.isApplicableTo(SplitAtomPatternIntention.kt:62) at org.arend.intention.SelfTargetingIntention.getTarget(SelfTargetingIntention.kt:62) at org.arend.intention.SelfTargetingIntention.isAvailable(SelfTargetingIntention.kt:78) at com.intellij.codeInsight.intention.impl.ShowIntentionActionsHandler.availableFor(ShowIntentionActionsHandler.java:169) at com.intellij.codeInsight.daemon.impl.ShowIntentionsPass.lambda$getActionsToShow$1(ShowIntentionsPass.java:339) at com.intellij.codeInsight.intention.impl.ShowIntentionActionsHandler.chooseBetweenHostAndInjected(ShowIntentionActionsHandler.java:202) at com.intellij.codeInsight.daemon.impl.ShowIntentionsPass.getActionsToShow(ShowIntentionsPass.java:338) at com.intellij.codeInsight.daemon.impl.ShowIntentionsPass.doCollectInformation(ShowIntentionsPass.java:242) at com.intellij.codeHighlighting.TextEditorHighlightingPass.collectInformation(TextEditorHighlightingPass.java:56) at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.lambda$doRun$1(PassExecutorService.java:419) at com.intellij.openapi.application.impl.ApplicationImpl.tryRunReadAction(ApplicationImpl.java:1152) at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.lambda$doRun$2(PassExecutorService.java:412) at com.intellij.openapi.progress.impl.CoreProgressManager.lambda$executeProcessUnderProgress$12(CoreProgressManager.java:608)...
