diff --git a/src/app/editor/editor.js b/src/app/editor/editor.js index 369eee5a0e..ea1a3fa4b8 100644 --- a/src/app/editor/editor.js +++ b/src/app/editor/editor.js @@ -207,11 +207,6 @@ class Editor extends Plugin { this.sourceHighlighters.discardHighlightAt(line, filePath, from) } - currentHighlights () { - const { from } = this.currentRequest - return this.sourceHighlighters.currentHighlights(from) - } - setTheme (type) { this.editor.setTheme('ace/theme/' + this._themes[type]) }