# HG changeset patch
# User wenzelm
# Date 1496137338 -7200
# Node ID 5d9da2f8fd3f459b2e53379053917d40ceb8994a
# Parent  169d2928cce1bc5de4624e1fbdbb9cfcce2d4d4b
clarified signature;

diff -r 169d2928cce1 -r 5d9da2f8fd3f src/Tools/VSCode/extension/src/library.ts
--- 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
 }
diff -r 169d2928cce1 -r 5d9da2f8fd3f src/Tools/VSCode/extension/src/preview.ts
--- 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(