--- a/src/Tools/VSCode/extension/src/preview.ts Tue Jun 06 23:13:53 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts Wed Jun 07 15:52:18 2017 +0200
@@ -80,7 +80,12 @@
if (preview_uri) {
preview_content.set(preview_uri.toString(), params.content)
content_provider.update(preview_uri)
- if (params.column != 0) {
+
+ const existing_document =
+ workspace.textDocuments.find(document =>
+ document.uri.scheme === preview_uri.scheme &&
+ document.uri.query === preview_uri.query)
+ if (!existing_document && params.column != 0) {
commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label)
}
}