improve UI

EshaanAgg · Jul 25, 2024 · 21697e7 · 21697e7
1 parent 7a45292
commit 21697e7
Show file tree

Hide file tree

Showing 2 changed files with 35 additions and 4 deletions.
diff --git a/benchexec/tablegenerator/react-table/src/components/StatisticsTable.js b/benchexec/tablegenerator/react-table/src/components/StatisticsTable.js
@@ -33,6 +33,15 @@ const StatisticsTable = ({ switchToQuantile, tableData, hiddenCols }) => {
             column={column}
             className="header-data clickable"
             title="Show Quantile Plot of this column"
+            style={{
+              cursor: "pointer",
+              padding: 0,
+              margin: 0,
+              alignContent: "center",
+              alignItems: "center",
+              backgroundColor: "#EEEEEE",
+              fontWeight: "bold",
+            }}
             onClick={(_) => switchToQuantile(column)}
           />
         ),
@@ -100,12 +109,21 @@ const StatisticsTable = ({ switchToQuantile, tableData, hiddenCols }) => {
     <div className="table-header">
       {headerGroups.map((headerGroup) => (
         <div className="tr headergroup" {...headerGroup.getHeaderGroupProps()}>
-          {headerGroup.headers.map((header) => (
+          {headerGroup.headers.map((header, index) => (
             <div
               {...header.getHeaderProps({
                 className: `th header ${header.headers ? "outer " : ""}${
                   header.className || ""
                 }`,
+                style: {
+                  margin: 0,
+                  padding: 0,
+                  borderLeft: index !== 0 ? "1px solid grey" : "none",
+                  borderRight:
+                    index !== headerGroup.headers.length - 1
+                      ? "1px solid grey"
+                      : "none",
+                },
               })}
             >
               {header.render("Header")}
@@ -126,14 +144,17 @@ const StatisticsTable = ({ switchToQuantile, tableData, hiddenCols }) => {
 
   const renderTableData = (rows) => (
     <div {...getTableBodyProps()} className="table-body body">
-      {rows.map((row) => {
+      {rows.map((row, index) => {
         prepareRow(row);
         return (
           <div {...row.getRowProps()} className="tr">
             {row.cells.map((cell) => (
               <div
                 {...cell.getCellProps({
                   className: "td " + (cell.column.className || ""),
+                  style: {
+                    backgroundColor: index % 2 === 0 ? "white" : "#EEEEEE",
+                  },
                 })}
               >
                 {cell.render("Cell")}

diff --git a/benchexec/tablegenerator/react-table/src/components/Summary.js b/benchexec/tablegenerator/react-table/src/components/Summary.js
@@ -136,7 +136,17 @@ const Summary = ({
     });
 
     colArray.push({
-      Header: <SelectColumnsButton handler={selectColumn} />,
+      Header: (
+        <SelectColumnsButton
+          handler={selectColumn}
+          style={{
+            border: "1px solid #DDD",
+            borderRadius: "5px",
+            width: "100%",
+            padding: "2px",
+          }}
+        />
+      ),
       id: "columnselect",
       accessor: "columnselect",
       statisticTable: true,
@@ -155,7 +165,7 @@ const Summary = ({
             statisticsRows[stats[stat].id].title +
             (filtered ? " of selected rows" : ""),
           stats: true,
-          width: 250,
+          minWidth: 300,
         });
       }
     }