# HG changeset patch
# User wenzelm
# Date 1497359461 -7200
# Node ID 441f95b05944f7f36281fbbe2c5e9b6b07661f61
# Parent  066f4ba9c9650f4b7ebdaca787642e6ec08c36ce
clarified modules;

diff -r 066f4ba9c965 -r 441f95b05944 src/Tools/VSCode/extension/src/library.ts
--- a/src/Tools/VSCode/extension/src/library.ts	Tue Jun 13 11:53:24 2017 +0200
+++ b/src/Tools/VSCode/extension/src/library.ts	Tue Jun 13 15:11:01 2017 +0200
@@ -1,7 +1,7 @@
 'use strict';
 
 import * as os from 'os';
-import { TextEditor, Uri, workspace } from 'vscode'
+import { TextEditor, Uri, ViewColumn, workspace } from 'vscode'
 
 
 /* regular expressions */
@@ -40,3 +40,15 @@
   const config = color + (light ? "_light" : "_dark") + "_color"
   return get_configuration<string>(config)
 }
+
+
+/* GUI */
+
+export function adjacent_editor_column(editor: TextEditor, split: boolean): ViewColumn
+{
+  if (!editor) return ViewColumn.One
+  else if (!split) return editor.viewColumn
+  else if (editor.viewColumn === ViewColumn.One || editor.viewColumn === ViewColumn.Three)
+    return ViewColumn.Two
+  else return ViewColumn.Three
+}
diff -r 066f4ba9c965 -r 441f95b05944 src/Tools/VSCode/extension/src/preview.ts
--- a/src/Tools/VSCode/extension/src/preview.ts	Tue Jun 13 11:53:24 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts	Tue Jun 13 15:11:01 2017 +0200
@@ -85,24 +85,14 @@
 
 /* commands */
 
-function preview_column(split: boolean): ViewColumn
-{
-  const active_editor = window.activeTextEditor
-
-  if (!active_editor) return ViewColumn.One
-  else if (!split) return active_editor.viewColumn
-  else if (active_editor.viewColumn === ViewColumn.One ||
-    active_editor.viewColumn === ViewColumn.Three) return ViewColumn.Two
-  else return ViewColumn.Three
-}
-
 export function request(uri?: Uri, split: boolean = false)
 {
   const document_uri = uri || window.activeTextEditor.document.uri
   const preview_uri = encode_preview(document_uri)
   if (preview_uri && language_client) {
     language_client.sendNotification(protocol.preview_request_type,
-      { uri: document_uri.toString(), column: preview_column(split) })
+      { uri: document_uri.toString(),
+        column: library.adjacent_editor_column(window.activeTextEditor, split) })
   }
 }