intellij-arend
intellij-arend copied to clipboard
Improve Arend Messages panel
Currently Arend Messages panel shows:
a) all error messages within all library files b) error messages are grouped with respect to the definition that contains them.
It would be helpful if
a) the scope of error messages would be configurable (i.e. let the user choose between the current file or all library files) b) the would be a possibility to choose whether the user wants to see error list as is or if he would like all errors to be shown ungrouped but sorted with respect to the position of error (line/column).