intellij-arend
intellij-arend copied to clipboard
JetBrains
Arend plugin for IntelliJ IDEA
``` java.lang.Throwable: Write-unsafe context! Model changes are allowed from write-safe contexts only. Please ensure you're using invokeLater/invokeAndWait with a correct modality state (not "any"). See TransactionGuard documentation for details. current...
In this code sample `true` and `false` should be highlighted as variables, whose names clash with the names of the (unimported) constructors of the datatype Bool. ``` \import Data.Bool(Bool, if)...
Currently one can not use numerals when formulating a search query in proof searcher.
If you select "{?}" and then push open parenthesis "(" the plugin returns "(?)" instead of "({?})", which I believe would be more useful and convenient
``` com.intellij.diagnostic.PluginException: PSI element is provided on EDT by com.intellij.ui.popup.PopupListAdapter$MyListWrapper.getData("selectedItem"). Please move that to a BGT data provider using PlatformCoreDataKeys.BGT_DATA_PROVIDER at com.intellij.diagnostic.PluginProblemReporterImpl.createPluginExceptionByClass(PluginProblemReporterImpl.java:23) at com.intellij.diagnostic.PluginException.createByClass(PluginException.java:90) at com.intellij.ide.impl.DataValidators.reportPsiElementOnEdt(DataValidators.java:96) at com.intellij.ide.impl.DataValidators.isDataValid(DataValidators.java:71) at com.intellij.ide.impl.DataValidators.validOrNull(DataValidators.java:64)...
In the updated Intellij IDEA interface there is a new breadcrumbs bar and it is currently not suported by Arend plugin: Arend (internal structure within the file is not shown):...
Currently the items listed in the File Structure menu (Alt+7) are not navigable in Arend (unlike their Java/Kotlin counterparts).
Unmarking directory as a source root sometimes does not always propagate this change to YAML file. In this gif there's an example of a correct behavior for arend-lib and an...