From 8f93f74600fb6b7f2bb2e5ea93a419e465f7cc34 Mon Sep 17 00:00:00 2001 From: yann300 Date: Mon, 17 Sep 2018 19:16:55 +0200 Subject: [PATCH] add discard highlight --- src/app/plugin/pluginAPI.js | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/app/plugin/pluginAPI.js b/src/app/plugin/pluginAPI.js index a6c8f8dd54..99a738e168 100644 --- a/src/app/plugin/pluginAPI.js +++ b/src/app/plugin/pluginAPI.js @@ -127,6 +127,10 @@ module.exports = (pluginManager, fileProviders, fileManager, compiler, udapp) => highlighter.currentSourceLocation(null) highlighter.currentSourceLocationFromfileName(position, filePath, hexColor) cb() + }, + discardHighlight: (mod, cb) => { + highlighter.currentSourceLocation(null) + cb() } } }