clarified signature;
authorwenzelm
Tue, 30 May 2017 11:42:18 +0200
changeset 65967 5d9da2f8fd3f
parent 65966 169d2928cce1
child 65968 44e703278dfd
clarified signature;
src/Tools/VSCode/extension/src/library.ts
src/Tools/VSCode/extension/src/preview.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
 }
--- 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(