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

header in local HTML-table without loading local Javascript not scrolling scroll left-right. #375

Closed
kfriedberger opened this issue Nov 20, 2018 · 1 comment · Fixed by #477
Closed

header in local HTML-table without loading local Javascript not scrolling scroll left-right. #375

kfriedberger opened this issue Nov 20, 2018 · 1 comment · Fixed by #477
Labels
enhancement HTML table

Comments

@kfriedberger
Copy link
Member

I know this case is weird, but I got a html-table for some tool via mail and opening it is not nice.
The table was created in local mode (or maybe downloaded from sosy-lab-server including all Javascript sources), such that all internal references to Javascript files are pointing to local files, which were not part of the mail :-(

When opening this local html-table, no Javascript-files are available and some features are missing. I am ok with that, because at least the table is readable.
However, all Javascript-related buttons are shown (and useless) and the header is floating (yes, that works partially). My problem is that the header does not move from riht to left when scrolling from left to right in larger tables. I can not read the right half of the header.

The wanted solution is

  • (important for me:) to deactivate the floating header if some important Javascript files are missing, and
  • (important for users in general:) to deactivate all buttons if Javascript cannot be loaded.
@PhilippWendler
Copy link
Member

The second is implemented since these buttons exist.

@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
2 participants
@PhilippWendler @kfriedberger