@ -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]) {
@ -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', [])
})