From 34b73c117bf4f655d963b05389b0f8ba2850f955 Mon Sep 17 00:00:00 2001
From: yann300 <yann.levreau@gmail.com>
Date: Tue, 19 May 2020 14:04:51 +0200
Subject: [PATCH] make sure to highlight using internal path

---
 src/app/editor/sourceHighlighter.js | 3 ++-
 src/app/files/fileManager.js        | 7 +++++--
 src/app/files/remixDProvider.js     | 8 ++++++++
 3 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/src/app/editor/sourceHighlighter.js b/src/app/editor/sourceHighlighter.js
index 4c52de3bc6..8b45d3dc49 100644
--- a/src/app/editor/sourceHighlighter.js
+++ b/src/app/editor/sourceHighlighter.js
@@ -39,8 +39,9 @@ class SourceHighlighter {
     this.source = null
     if (lineColumnPos) {
       this.source = filePath
-      if (this._deps.config.get('currentFile') !== this.source) {
+      if (this._deps.fileManager.currentFile() !== this.source) {
         await this._deps.fileManager.open(this.source)
+        this.source = this._deps.fileManager.currentFile()
       }
 
       const css = csjs`
diff --git a/src/app/files/fileManager.js b/src/app/files/fileManager.js
index 88de90bed1..4a2d6a6f96 100644
--- a/src/app/files/fileManager.js
+++ b/src/app/files/fileManager.js
@@ -432,13 +432,16 @@ class FileManager extends Plugin {
   openFile (file) {
     const _openFile = (file) => {
       this.saveCurrentFile()
+      const provider = this.fileProviderOf(file)
+      if (!provider) return console.error(`no provider for ${file}`)
+      file = provider.getPathFromUrl(file) || file // in case an external URL is given as input, we resolve it to the right internal path
       this._deps.config.set('currentFile', file)
       this.openedFiles[file] = file
-      this.fileProviderOf(file).get(file, (error, content) => {
+      provider.get(file, (error, content) => {
         if (error) {
           console.log(error)
         } else {
-          if (this.fileProviderOf(file).isReadOnly(file)) {
+          if (provider.isReadOnly(file)) {
             this.editor.openReadOnly(file, content)
           } else {
             this.editor.open(file, content)
diff --git a/src/app/files/remixDProvider.js b/src/app/files/remixDProvider.js
index d4c9ac866a..15df112559 100644
--- a/src/app/files/remixDProvider.js
+++ b/src/app/files/remixDProvider.js
@@ -89,6 +89,14 @@ module.exports = class RemixDProvider {
     return cb(null, result)
   }
 
+  getNormalizedName (path) {
+    return path
+  }
+
+  getPathFromUrl (path) {
+    return path
+  }
+
   get (path, cb) {
     var unprefixedpath = this.removePrefix(path)
     this._remixd.call('sharedfolder', 'get', {path: unprefixedpath}, (error, file) => {