# HG changeset patch # User wenzelm # Date 1496137228 -7200 # Node ID 169d2928cce1bc5de4624e1fbdbb9cfcce2d4d4b # Parent 3de7464450b045c81b5457c8144f267923fc312d clarified modules; diff -r 3de7464450b0 -r 169d2928cce1 src/Tools/VSCode/extension/src/library.ts --- /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 +} diff -r 3de7464450b0 -r 169d2928cce1 src/Tools/VSCode/extension/src/preview.ts --- 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(