# HG changeset patch
# User wenzelm
# Date 1496079247 -7200
# Node ID 47309113ee4d7a42c7a50d38ec08eeca24f6e9af
# Parent  6338355b2a88a9973418604d1ed8a1876ab2624b
clarified view column;
tuned whitespace;

diff -r 6338355b2a88 -r 47309113ee4d src/Tools/VSCode/extension/src/preview.ts
--- a/src/Tools/VSCode/extension/src/preview.ts	Mon May 29 15:16:32 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts	Mon May 29 19:34:07 2017 +0200
@@ -1,6 +1,6 @@
 'use strict';
 
-import { TextDocumentContentProvider, ExtensionContext, Uri, Position,
+import { TextDocumentContentProvider, ExtensionContext, Uri, Position, ViewColumn,
   workspace, window, commands } from 'vscode'
 
 
@@ -8,7 +8,7 @@
 
 class Provider implements TextDocumentContentProvider
 {
-	constructor() { }
+  constructor() { }
 
   dispose() { }
 
@@ -27,8 +27,19 @@
 
 export function decode_location(uri: Uri): [Uri, Position]
 {
-	let [name, line, character] = <[string, number, number]>JSON.parse(uri.query)
-	return [Uri.parse(name), new Position(line, character)]
+  let [name, line, character] = <[string, number, number]>JSON.parse(uri.query)
+  return [Uri.parse(name), new Position(line, character)]
+}
+
+function view_column(side_by_side: boolean = true): ViewColumn | undefined
+{
+  const active = window.activeTextEditor
+  if (!active) { return ViewColumn.One }
+  if (!side_by_side) { return active.viewColumn }
+
+  if (active.viewColumn == ViewColumn.One) return ViewColumn.Two
+  else if (active.viewColumn == ViewColumn.Two) return ViewColumn.Three
+  else return ViewColumn.One
 }
 
 export function init(context: ExtensionContext)
@@ -38,12 +49,12 @@
   const provider_registration =
     workspace.registerTextDocumentContentProvider(uri_scheme, provider)
 
- 	const command_registration =
+  const command_registration =
     commands.registerTextEditorCommand("isabelle.preview", editor =>
     {
       const uri = encode_location(editor.document.uri, editor.selection.active)
-      return workspace.openTextDocument(uri).then(doc => window.showTextDocument(doc, editor.viewColumn + 1))
-  	})
+      return workspace.openTextDocument(uri).then(doc => window.showTextDocument(doc, view_column()))
+    })
 
   context.subscriptions.push(provider, provider_registration, command_registration)
 }