parent
0b540fbabd
commit
579750fbc0
|
@ -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);
|
||||
|
|
|
@ -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) {
|
||||
|
|
Loading…
Reference in New Issue
Block a user