clarified modules;
authorwenzelm
Tue, 30 May 2017 11:40:28 +0200
changeset 65966 169d2928cce1
parent 65964 3de7464450b0
child 65967 5d9da2f8fd3f
clarified modules;
src/Tools/VSCode/extension/src/library.ts
src/Tools/VSCode/extension/src/preview.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
+}
--- 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(