--- a/src/Tools/VSCode/extension/src/library.ts Tue May 30 11:40:28 2017 +0200
+++ b/src/Tools/VSCode/extension/src/library.ts Tue May 30 11:42:18 2017 +0200
@@ -1,12 +1,11 @@
'use strict';
-import { ViewColumn, window } from 'vscode'
+import { ViewColumn, TextEditor } from 'vscode'
-export function other_column(): ViewColumn
+export function other_column(active_editor: TextEditor | null): ViewColumn
{
- const active = window.activeTextEditor
- if (!active || active.viewColumn === ViewColumn.Three) return ViewColumn.One
- else if (active.viewColumn === ViewColumn.One) return ViewColumn.Two
+ if (!active_editor || active_editor.viewColumn === ViewColumn.Three) return ViewColumn.One
+ else if (active_editor.viewColumn === ViewColumn.One) return ViewColumn.Two
else return ViewColumn.Three
}
--- a/src/Tools/VSCode/extension/src/preview.ts Tue May 30 11:40:28 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts Tue May 30 11:42:18 2017 +0200
@@ -75,7 +75,7 @@
const preview_uri = encode_name(editor.document.uri)
return workspace.openTextDocument(preview_uri).then(doc =>
commands.executeCommand("vscode.previewHtml", preview_uri,
- library.other_column(), "Isabelle Preview"))
+ library.other_column(window.activeTextEditor), "Isabelle Preview"))
}))
context.subscriptions.push(