From 735c4e548dc6ab4d503632cdee14be770ea5bb7c Mon Sep 17 00:00:00 2001 From: yann300 Date: Thu, 3 Aug 2017 11:23:43 +0200 Subject: [PATCH] remove / add marker with source --- src/app.js | 16 +++++++++------- src/app/editor.js | 13 +++++++++---- 2 files changed, 18 insertions(+), 11 deletions(-) diff --git a/src/app.js b/src/app.js index 5063808636..2d3594ffc8 100644 --- a/src/app.js +++ b/src/app.js @@ -748,17 +748,19 @@ function run () { var debugAPI = { statementMarker: null, fullLineMarker: null, + source: null, currentSourceLocation: (lineColumnPos, location) => { - if (this.statementMarker) editor.removeMarker(this.statementMarker) - if (this.fullLineMarker) editor.removeMarker(this.fullLineMarker) + if (this.statementMarker) editor.removeMarker(this.statementMarker, this.source) + if (this.fullLineMarker) editor.removeMarker(this.fullLineMarker, this.source) this.statementMarker = null this.fullLineMarker = null + this.source = null if (lineColumnPos) { - var source = compiler.lastCompilationResult.data.sourceList[location.file] // auto switch to that tab - if (config.get('currentFile') !== source) { - switchToFile(source) + this.source = compiler.lastCompilationResult.data.sourceList[location.file] // auto switch to that tab + if (config.get('currentFile') !== this.source) { + switchToFile(this.source) } - this.statementMarker = editor.addMarker(lineColumnPos, 'highlightcode') + this.statementMarker = editor.addMarker(lineColumnPos, this.source, 'highlightcode') editor.scrollToLine(lineColumnPos.start.line, true, true, function () {}) if (lineColumnPos.start.line === lineColumnPos.end.line) { @@ -771,7 +773,7 @@ function run () { line: lineColumnPos.start.line + 1, column: 0 } - }, 'highlightcode_fullLine') + }, this.source, 'highlightcode_fullLine') } } }, diff --git a/src/app/editor.js b/src/app/editor.js index 19ffda7088..a4cb8379ac 100644 --- a/src/app/editor.js +++ b/src/app/editor.js @@ -148,17 +148,22 @@ function Editor (opts = {}) { } } - this.addMarker = function (lineColumnPos, cssClass) { + this.addMarker = function (lineColumnPos, source, cssClass) { var currentRange = new Range(lineColumnPos.start.line, lineColumnPos.start.column, lineColumnPos.end.line, lineColumnPos.end.column) - return editor.session.addMarker(currentRange, cssClass) + if (sessions[source]) { + return sessions[source].addMarker(currentRange, cssClass) + } + return null } this.scrollToLine = function (line, center, animate, callback) { editor.scrollToLine(line, center, animate, callback) } - this.removeMarker = function (markerId) { - editor.session.removeMarker(markerId) + this.removeMarker = function (markerId, source) { + if (sessions[source]) { + sessions[source].removeMarker(markerId) + } } this.clearAnnotations = function () {