diff --git a/edit/linter.js b/edit/linter.js index 35ad28a0..67f11399 100644 --- a/edit/linter.js +++ b/edit/linter.js @@ -29,6 +29,7 @@ const linter = (() => { * update when lint gutter is added to a lot of editors simultaneously. */ enableForEditor(cm, code) { + if (cms.has(cm)) return; if (code) return enableOnProblems(cm, code); cm.setOption('lint', {getAnnotations, onUpdateLinting}); cms.add(cm); diff --git a/edit/sections-editor.js b/edit/sections-editor.js index f0bf08fe..8405cbb6 100644 --- a/edit/sections-editor.js +++ b/edit/sections-editor.js @@ -651,8 +651,11 @@ function SectionsEditor() { } function refreshOnView(cm, {code, force} = {}) { + if (code) { + linter.enableForEditor(cm, code); + } if (force || !xo) { - refreshOnViewNow(cm, code); + refreshOnViewNow(cm); } else { xo.observe(cm.display.wrapper); } @@ -674,9 +677,9 @@ function SectionsEditor() { } } - async function refreshOnViewNow(cm, code) { + async function refreshOnViewNow(cm) { + linter.enableForEditor(cm); cm.refresh(); - linter.enableForEditor(cm, code); } function toggleContextMenuDelete(event) {