|
|
@ -31,7 +31,7 @@ class SourceHighlighter { |
|
|
|
} |
|
|
|
} |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
async currentSourceLocationFromfileName (lineColumnPos, filePath, style) { |
|
|
|
currentSourceLocationFromfileName (lineColumnPos, filePath, style) { |
|
|
|
if (this.statementMarker) this._deps.editor.removeMarker(this.statementMarker, this.source) |
|
|
|
if (this.statementMarker) this._deps.editor.removeMarker(this.statementMarker, this.source) |
|
|
|
if (this.fullLineMarker) this._deps.editor.removeMarker(this.fullLineMarker, this.source) |
|
|
|
if (this.fullLineMarker) this._deps.editor.removeMarker(this.fullLineMarker, this.source) |
|
|
|
this.statementMarker = null |
|
|
|
this.statementMarker = null |
|
|
@ -40,7 +40,7 @@ class SourceHighlighter { |
|
|
|
if (lineColumnPos) { |
|
|
|
if (lineColumnPos) { |
|
|
|
this.source = filePath |
|
|
|
this.source = filePath |
|
|
|
if (this._deps.config.get('currentFile') !== this.source) { |
|
|
|
if (this._deps.config.get('currentFile') !== this.source) { |
|
|
|
await this._deps.fileManager.switchFile(this.source) |
|
|
|
this._deps.fileManager.switchFile(this.source) |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
const css = csjs` |
|
|
|
const css = csjs` |
|
|
|