shorten section labels in lint report

This commit is contained in:
tophf 2022-02-04 17:55:37 +03:00
parent e11c4ef755
commit aad4828e4a
3 changed files with 25 additions and 15 deletions

View File

@ -849,26 +849,29 @@ body:not(.find-open) [data-match-highlight-count="1"] .CodeMirror-selection-high
#lint td[role="line"] { #lint td[role="line"] {
padding-left: 0.25rem; padding-left: 0.25rem;
} }
#lint table:last-child { #lint .empty {
margin-bottom: 0;
}
#lint table.empty {
display: none; display: none;
} }
#lint caption:not(:empty) { #lint .caption {
text-align: left; vertical-align: top;
line-height: 16px;
font-weight: bold; font-weight: bold;
padding-bottom: 6px;
} }
#lint tbody { #lint .report {
font-size: 85%; font-size: 85%;
cursor: pointer; 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); background-color: hsla(180, 50%, 36%, .2);
} }
#lint td { #lint td {
padding: 0; padding: 0;
line-height: 16px;
} }
#lint td[role="severity"] { #lint td[role="severity"] {
font-size: 0; font-size: 0;

View File

@ -328,9 +328,13 @@ linterMan.DEFAULTS = {
} }
function createTable(cm) { function createTable(cm) {
const caption = $create('caption'); const caption = $create('td.caption');
const tbody = $create('tbody'); const tbody = $create('tbody.report');
const table = $create('table', [caption, tbody]); const table = $create('table',
$create('tr', [
caption,
$create('td', tbody),
]));
const trs = []; const trs = [];
return { return {
element: table, element: table,
@ -340,7 +344,7 @@ linterMan.DEFAULTS = {
}; };
function updateCaption() { function updateCaption() {
caption.textContent = editor.getEditorTitle(cm); Object.assign(caption, editor.getEditorTitle(cm));
} }
function updateAnnotations(lines) { function updateAnnotations(lines) {

View File

@ -46,8 +46,11 @@ function SectionsEditor() {
}, },
getEditorTitle(cm) { getEditorTitle(cm) {
const index = editor.getEditors().indexOf(cm); const index = editor.getEditors().indexOf(cm) + 1;
return `${t('sectionCode')} ${index + 1}`; return {
textContent: `#${index}`,
title: `${t('sectionCode')} ${index}`,
};
}, },
getValue(asObject) { getValue(asObject) {