benchexec icon indicating copy to clipboard operation
benchexec copied to clipboard

Filter for only differing and only equal rows in HTML tables

Open PhilippWendler opened this issue 9 years ago • 2 comments

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.

PhilippWendler avatar Feb 09 '16 10:02 PhilippWendler

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.

PhilippWendler avatar Nov 18 '19 14:11 PhilippWendler

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.

PhilippWendler avatar Feb 03 '22 10:02 PhilippWendler