ensure file is opened before marking it

src/app/editor/sourceHighlighter.js

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