Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Manual selection of header rows in HTML tables #296

Closed
PhilippWendler opened this issue Apr 22, 2018 · 0 comments · Fixed by #477
Closed

Manual selection of header rows in HTML tables #296

PhilippWendler opened this issue Apr 22, 2018 · 0 comments · Fixed by #477
Labels
enhancement HTML table

Comments

@PhilippWendler
Copy link
Member

In some cases, like for SV-COMP, the header of HTML tables is still large even after clicking "Shrink Header". However, other rows in the header would be sufficient for the user to distinguish the columns. Thus, it could be useful for the user to be able to choose manually which header rows to show (could be integrated in the "Filter Rows" dialog, e.g., with a checkbox for each header row).
@PhilippWendler PhilippWendler mentioned this issue Apr 22, 2018
Closed
@PhilippWendler PhilippWendler mentioned this issue Nov 1, 2019
Merged
PhilippWendler added a commit that referenced this issue Nov 2, 2019
@PhilippWendler
Rewrite of HTML tables with React (#477)
d20b13b 
This provides a complete rewrite of the HTML tables that `table-generator` produces. Instead of statically creating a HTML `<table>`, we now insert the data as JSON and use [React](https://reactjs.org/) to render a table dynamically. Furthermore, all the spaghetti code for interactive features like plots is now completely replaced by a proper architecture using React components, and there exists infrastructure to test this.

Some new features like better row filters and improvements have also been added based on a user study. But the main advantage is that it is now possible to open large tables in browsers without long waiting periods.

The studies and the rewrite were done by @bschor and a report about this is available as her [Bachelor's thesis](https://www.sosy-lab.org/research/bsc/2019.Bschor.Modern_Architecture_and_Improved_UI_for_Tables_of_BenchExec.pdf).

Users who whish to continue using the old tables can pass `--static-table` to `table-generator`, but we expect this to be removed in BenchExec 3.0.

Fixes #130 (sorting added)
Fixes #423 (summary tab with only header and footer of table added)
Closes #123 (all Javascript is now bundled in the HTML file)
Closes #195 (all Javascript is now bundled in the HTML file)
Closes #214 (filtering is now longer in an overlay, and much faster anyway)
Closes #237 ([react-table](https://www.npmjs.com/package/react-table) is used)
Closes #296 (main table has only small header, full header is shown on summary tab)
Closes #297 (main table has only small header, full header is shown on summary tab)
Closes #375 (no longer applicable)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement HTML table
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Rewrite of HTML tables with React sosy-lab/benchexec
1 participant
@PhilippWendler