-
Notifications
You must be signed in to change notification settings - Fork 2
Open
Labels
enhancementNew feature or requestNew feature or request
Description
Errors that occur after pressing the play button do currently appear as magenta-colored fixed-width text. Errors have headings of the form
[202] Error: unsafe variable used in rule head: '?x'
This display could be improved as follows:
- Change font color to black
- Change style of error headings to be more prominent and not fixed-width; maybe put a (collapsible?) box around each error to group them more prominently
- Remove the overall headline "Errors". Now that the errors have individual headlines, this should be clear enough
- Change the way in which the error code is displayed ("[202]" above) so that it is not the first thing in the line, and so that it is more clear that this is an internal error code (is it actually relevant to the user at all?)
The fixed-width display of the error location can stay. No need to HTML-ify this, given that we have an editor above.
Metadata
Metadata
Assignees
Labels
enhancementNew feature or requestNew feature or request
Type
Projects
Status
Todo