Polish leaderboard table layout

app.py

@@ -241,23 +241,22 @@ def filter_table(view: str, metric: str, family: str, query: str, top_n: int):
     ascending = not HIGHER_IS_BETTER.get(metric, True)
     ranked = df.sort_values(metric, ascending=ascending, na_position="last").head(int(top_n))
 
-    show_cols = [
-        col
-        for col in [
-            "rank",
-            "display_name",
-            "method",
-            "family",
-            "dataset",
-            metric,
-            "mean_metric_rank",
-            "overall_mean_rank",
-            "coverage_success",
-            "row_count",
-            "setting_count",
-        ]
-        if col in ranked.columns
-    ]
+    show_cols = []
+    for col in [
+        "rank",
+        "display_name",
+        "method",
+        "family",
+        "dataset",
+        metric,
+        "mean_metric_rank",
+        "overall_mean_rank",
+        "coverage_success",
+        "row_count",
+        "setting_count",
+    ]:
+        if col in ranked.columns and col not in show_cols:
+            show_cols.append(col)
     remaining_metrics = [
         col
         for col in ranked.columns
@@ -394,7 +393,14 @@ with gr.Blocks(**BLOCKS_KWARGS) as demo:
 
     note = gr.Markdown()
     plot = gr.Plot()
-    table = gr.Dataframe(label="Leaderboard table", wrap=True, interactive=False)
+    table = gr.Dataframe(
+        label="Leaderboard table",
+        wrap=False,
+        interactive=False,
+        max_height=520,
+        column_widths=["72px", "230px", "220px", "150px", "140px", "150px"],
+        show_search="filter",
+    )
 
     inputs = [view, metric, family, query, top_n]
     for control in inputs: