From 579750fbc0ceec5194436c0b1db7293df151c9d0 Mon Sep 17 00:00:00 2001
From: tophf <tophf@gmx.com>
Date: Thu, 10 Dec 2020 10:59:28 +0300
Subject: [PATCH] fix linting when style was initially error-free

regressed in e6f94378
---
 edit/linter.js          | 1 +
 edit/sections-editor.js | 9 ++++++---
 2 files changed, 7 insertions(+), 3 deletions(-)

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) {