benchexec
benchexec copied to clipboard
Filter for only differing and only equal rows in HTML tables
The "Filter Rows" possibility should be extended to allow easily filtering for rows that have differing values in their status
columns, just like the "diff" table that table-generator also produces.
The negation of this filter (only rows where all status
values are equal) can be also useful for graphs and statistics and should thus also be added.
We need to find a place in the UI for this, because now the filters are configured in a column-specific manner, and the proposed kind of filters would be global.
We could do this on the summary page, or maybe in some kind of popup menu that is accessible via the upper right corner (together with the "reset" button)? Potentially we could also create a new "Filters" tab, which duplicate the functionality of the existing column filters and also provide these global filters.
For the record: Since the introduction of the filter sidebar, there is an obvious way where to add the UI for this: On the very top of the filter side bar.