Reduce page size and number of DOM elements on clippy lints page

Author: GuillaumeGomez

util/gh-pages/index_template.html

@@ -149,25 +149,21 @@ <h1>Clippy Lints <span id="lint-count" class="badge"></span></h1> {# #}
                 <article class="panel panel-default" id="{{lint.id}}"> {# #}
                     <input id="label-{{lint.id}}" type="checkbox"> {# #}
                     <label for="label-{{lint.id}}"> {# #}
-                        <header class="panel-heading"> {# #}
-                            <h2 class="panel-title"> {# #}
-                                <div class="panel-title-name" id="lint-{{lint.id}}"> {# #}
-                                    <span>{{lint.id}}</span> {#+ #}
-                                    <a href="#{{lint.id}}" class="lint-anchor anchor label label-default">&para;</a> {#+ #}
-                                    <a href="" class="copy-to-clipboard anchor label label-default"> {# #}
-                                        &#128203; {# #}
-                                    </a> {# #}
-                                </div> {# #}
+                        <h2 class="lint-title"> {# #}
+                            <div class="panel-title-name" id="lint-{{lint.id}}"> {# #}
+                                <span>{{lint.id}}</span> {#+ #}
+                                <a href="#{{lint.id}}" class="lint-anchor anchor label label-default">&para;</a> {#+ #}
+                                <a href="" class="copy-to-clipboard anchor label label-default"> {# #}
+                                    &#128203; {# #}
+                                </a> {# #}
+                            </div> {# #}
 
-                                <div class="panel-title-addons"> {# #}
-                                    <span class="label label-lint-group label-default label-group-{{lint.group}}">{{lint.group}}</span> {#+ #}
+                            <span class="label label-lint-group label-default label-group-{{lint.group}}">{{lint.group}}</span> {#+ #}
 
-                                    <span class="label label-lint-level label-lint-level-{{lint.level}}">{{lint.level}}</span> {#+ #}
+                            <span class="label label-lint-level label-lint-level-{{lint.level}}">{{lint.level}}</span> {#+ #}
 
-                                    <span class="label label-doc-folding"></span> {# #}
-                                </div> {# #}
-                            </h2> {# #}
-                        </header> {# #}
+                            <span class="label label-doc-folding"></span> {# #}
+                        </h2> {# #}
                     </label> {# #}
 
                     <div class="list-group lint-docs"> {# #}

util/gh-pages/style.css

@@ -50,8 +50,23 @@ div.panel div.panel-body  button.open {
 
 .panel-heading { cursor: pointer; }
 
-.panel-title { display: flex; flex-wrap: wrap;}
-.panel-title .label { display: inline-block; }
+.lint-title {
+    cursor: pointer;
+    margin-top: 0;
+    margin-bottom: 0;
+    font-size: 16px;
+    display: flex;
+    flex-wrap: wrap;
+    background: var(--theme-hover);
+    color: var(--fg);
+    border: 1px solid var(--theme-popup-border);
+    padding: 10px 15px;
+    border-top-left-radius: 3px;
+    border-top-right-radius: 3px;
+    gap: 4px;
+}
+
+.lint-title .label { display: inline-block; }
 
 .panel-title-name { flex: 1; min-width: 400px;}
 .panel-title-name span { vertical-align: bottom; }