From aad4828e4a1c96ec2086b2a79ad97129723460f9 Mon Sep 17 00:00:00 2001
From: tophf <tophf@gmx.com>
Date: Fri, 4 Feb 2022 17:55:37 +0300
Subject: [PATCH] shorten section labels in lint report

---
 edit/edit.css           | 21 ++++++++++++---------
 edit/linter-manager.js  | 12 ++++++++----
 edit/sections-editor.js |  7 +++++--
 3 files changed, 25 insertions(+), 15 deletions(-)

diff --git a/edit/edit.css b/edit/edit.css
index e771619e..f7dd4169 100644
--- a/edit/edit.css
+++ b/edit/edit.css
@@ -849,26 +849,29 @@ body:not(.find-open) [data-match-highlight-count="1"] .CodeMirror-selection-high
 #lint td[role="line"] {
   padding-left: 0.25rem;
 }
-#lint table:last-child {
-  margin-bottom: 0;
-}
-#lint table.empty {
+#lint .empty {
   display: none;
 }
-#lint caption:not(:empty) {
-  text-align: left;
+#lint .caption {
+  vertical-align: top;
+  line-height: 16px;
   font-weight: bold;
-  padding-bottom: 6px;
 }
-#lint tbody {
+#lint .report {
   font-size: 85%;
   cursor: pointer;
 }
-#lint tr:hover {
+.lint-report-container > :not(.empty) ~ :not(.empty) {
+  border-top: 1px dotted rgba(128, 128, 128, .5);
+  margin-top: .25em;
+  padding-top: .25em;
+}
+#lint .report tr:hover {
   background-color: hsla(180, 50%, 36%, .2);
 }
 #lint td {
   padding: 0;
+  line-height: 16px;
 }
 #lint td[role="severity"] {
   font-size: 0;
diff --git a/edit/linter-manager.js b/edit/linter-manager.js
index d6b65a71..faccced0 100644
--- a/edit/linter-manager.js
+++ b/edit/linter-manager.js
@@ -328,9 +328,13 @@ linterMan.DEFAULTS = {
   }
 
   function createTable(cm) {
-    const caption = $create('caption');
-    const tbody = $create('tbody');
-    const table = $create('table', [caption, tbody]);
+    const caption = $create('td.caption');
+    const tbody = $create('tbody.report');
+    const table = $create('table',
+      $create('tr', [
+        caption,
+        $create('td', tbody),
+      ]));
     const trs = [];
     return {
       element: table,
@@ -340,7 +344,7 @@ linterMan.DEFAULTS = {
     };
 
     function updateCaption() {
-      caption.textContent = editor.getEditorTitle(cm);
+      Object.assign(caption, editor.getEditorTitle(cm));
     }
 
     function updateAnnotations(lines) {
diff --git a/edit/sections-editor.js b/edit/sections-editor.js
index edcf569c..60b07151 100644
--- a/edit/sections-editor.js
+++ b/edit/sections-editor.js
@@ -46,8 +46,11 @@ function SectionsEditor() {
     },
 
     getEditorTitle(cm) {
-      const index = editor.getEditors().indexOf(cm);
-      return `${t('sectionCode')} ${index + 1}`;
+      const index = editor.getEditors().indexOf(cm) + 1;
+      return {
+        textContent: `#${index}`,
+        title: `${t('sectionCode')} ${index}`,
+      };
     },
 
     getValue(asObject) {