Fix #126 line number spacing not updating on zoom

This also fixes the cursor and selected line spacing not updating, which
is most obvious whet adjusting the line spacing.
Manually firing a refresh event for selectLanguage is not necessary as
it calls editor.setOption which fires this event internally.
This commit is contained in:
qqii 2023-01-08 02:37:22 +00:00
parent 7a1d1da331
commit d24ea63120
1 changed files with 2 additions and 0 deletions

View File

@ -81,12 +81,14 @@ function setSize() {
document.querySelector('.CodeMirror').style.fontSize = `${size}px`;
document.cookie = `size=${size};max-age=172800`;
editor.refresh();
}
function setSpacing() {
var spacing = document.getElementById('spacing').value;
document.querySelector('.CodeMirror').style.lineHeight = spacing;
document.cookie = `spacing=${spacing};max-age=172800`;
editor.refresh();
}
function selectLanguage() {
var lang = document.getElementById('select-language').value;