From 7fed76ae82f4c39597de43db072941c13ec41101 Mon Sep 17 00:00:00 2001 From: yann300 Date: Thu, 8 Feb 2018 12:34:55 +0100 Subject: [PATCH] add discardCurrentSession fn --- src/app/editor/editor.js | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/app/editor/editor.js b/src/app/editor/editor.js index 88272973ff..10e83e0f16 100644 --- a/src/app/editor/editor.js +++ b/src/app/editor/editor.js @@ -186,6 +186,13 @@ function Editor (opts = {}) { return editor.session.doc.positionToIndex(editor.getCursorPosition(), 0) } + this.discardCurrentSession = function () { + if (sessions[currentSession]) { + delete sessions[currentSession] + currentSession = null + } + } + this.discard = function (path) { if (currentSession !== path) { delete sessions[path]