JetBrains / intellij-arend

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

Improve Arend Messages panel #561

Open sxhya opened 1 month ago

sxhya commented 1 month ago

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).