From 129bf2e6d073f604bd07fa8a7d7e31ad90045e3e Mon Sep 17 00:00:00 2001
From: yann300 <yann.levreau@gmail.com>
Date: Tue, 19 May 2020 10:27:53 +0200
Subject: [PATCH] ensure file is opened before marking it

---
 src/app/editor/sourceHighlighter.js | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/app/editor/sourceHighlighter.js b/src/app/editor/sourceHighlighter.js
index 0b3989706c..4c52de3bc6 100644
--- a/src/app/editor/sourceHighlighter.js
+++ b/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`