remove / add marker with source

pull/1/head
yann300 7 years ago
parent 46a5ab53a1
commit 735c4e548d
  1. 16
      src/app.js
  2. 13
      src/app/editor.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')
}
}
},

@ -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 () {

Loading…
Cancel
Save