--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/library.ts Tue May 30 11:40:28 2017 +0200
@@ -0,0 +1,12 @@
+'use strict';
+
+import { ViewColumn, window } from 'vscode'
+
+
+export function other_column(): ViewColumn
+{
+ const active = window.activeTextEditor
+ if (!active || active.viewColumn === ViewColumn.Three) return ViewColumn.One
+ else if (active.viewColumn === ViewColumn.One) return ViewColumn.Two
+ else return ViewColumn.Three
+}
--- a/src/Tools/VSCode/extension/src/preview.ts Tue May 30 11:12:00 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts Tue May 30 11:40:28 2017 +0200
@@ -1,7 +1,9 @@
'use strict';
import { TextDocumentContentProvider, ExtensionContext, Event, EventEmitter, Uri, Position,
- ViewColumn, workspace, window, commands } from 'vscode'
+ workspace, window, commands } from 'vscode'
+
+import * as library from './library'
const uri_scheme = 'isabelle-preview';
@@ -61,14 +63,6 @@
return Uri.parse(name)
}
-function other_column(): ViewColumn
-{
- const active = window.activeTextEditor
- if (!active || active.viewColumn === ViewColumn.Three) return ViewColumn.One
- else if (active.viewColumn === ViewColumn.One) return ViewColumn.Two
- else return ViewColumn.Three
-}
-
export function init(context: ExtensionContext)
{
const provider = new Provider()
@@ -80,7 +74,8 @@
{
const preview_uri = encode_name(editor.document.uri)
return workspace.openTextDocument(preview_uri).then(doc =>
- commands.executeCommand("vscode.previewHtml", preview_uri, other_column(), "Isabelle Preview"))
+ commands.executeCommand("vscode.previewHtml", preview_uri,
+ library.other_column(), "Isabelle Preview"))
}))
context.subscriptions.push(