From 8a697216a4731469846299e970ae42c1e213db05 Mon Sep 17 00:00:00 2001 From: yann300 Date: Mon, 11 May 2020 12:18:45 +0200 Subject: [PATCH] remove uneeded fn --- src/app/editor/editor.js | 5 ----- 1 file changed, 5 deletions(-) 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]) }