From 939fa3ea2a4f0760f285fc435f3e129fd5ce3016 Mon Sep 17 00:00:00 2001
From: yann300 <yann.levreau@gmail.com>
Date: Thu, 5 Nov 2020 10:11:36 +0100
Subject: [PATCH] remove highlights if content changes

---
 apps/remix-ide/src/app/editor/SourceHighlighters.js | 6 ++++++
 apps/remix-ide/src/app/editor/editor.js             | 1 +
 2 files changed, 7 insertions(+)

diff --git a/apps/remix-ide/src/app/editor/SourceHighlighters.js b/apps/remix-ide/src/app/editor/SourceHighlighters.js
index 1cb6a15576..203a612dd2 100644
--- a/apps/remix-ide/src/app/editor/SourceHighlighters.js
+++ b/apps/remix-ide/src/app/editor/SourceHighlighters.js
@@ -50,6 +50,12 @@ class SourceHighlighters {
     this.highlighters[from] = []
   }
 
+  discardAllHighlights () {
+    for (const from in this.highlighters) {
+      this.discardHighlight(from)
+    }
+  }
+
   hideHighlightsExcept (toStay) {
     for (const highlighter in this.highlighters) {
       for (const index in this.highlighters[highlighter]) {
diff --git a/apps/remix-ide/src/app/editor/editor.js b/apps/remix-ide/src/app/editor/editor.js
index 2fbe481293..1d32e52bf7 100644
--- a/apps/remix-ide/src/app/editor/editor.js
+++ b/apps/remix-ide/src/app/editor/editor.js
@@ -191,6 +191,7 @@ class Editor extends Plugin {
       this.event.trigger('sessionSwitched', [])
       this.editor.getSession().on('change', () => {
         this._onChange()
+        this.sourceHighlighters.discardAllHighlights()
         this.event.trigger('contentChanged', [])
       })
     })