Skip to content

Improve Arend Messages panel #561

@sxhya

Description

@sxhya

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

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions