# HG changeset patch
# User wenzelm
# Date 1496138093 -7200
# Node ID 1f93eb5c3d770dfcea597cd74b076d2bd5440c9d
# Parent  44e703278dfda09bd64b5d9ce3f778f1a416e134
tuned imports;

diff -r 44e703278dfd -r 1f93eb5c3d77 src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Tue May 30 11:50:12 2017 +0200
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Tue May 30 11:54:53 2017 +0200
@@ -1,7 +1,7 @@
 'use strict';
 
 import * as timers from 'timers';
-import * as vscode from 'vscode'
+import { window, OverviewRulerLane } from 'vscode'
 import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions,
   TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
 import { Decoration } from './protocol'
@@ -73,7 +73,7 @@
 {
   function decoration(options: DecorationRenderOptions): TextEditorDecorationType
   {
-    const typ = vscode.window.createTextEditorDecorationType(options)
+    const typ = window.createTextEditorDecorationType(options)
     context.subscriptions.push(typ)
     return typ
   }
@@ -95,7 +95,7 @@
   function text_overview_color(color: string): TextEditorDecorationType
   {
     return decoration(
-      { overviewRulerLane: vscode.OverviewRulerLane.Right,
+      { overviewRulerLane: OverviewRulerLane.Right,
         light: { overviewRulerColor: library.get_color(color, true) },
         dark: { overviewRulerColor: library.get_color(color, false) } })
   }
@@ -113,7 +113,7 @@
 
   types.forEach(typ =>
   {
-    for (const editor of vscode.window.visibleTextEditors) {
+    for (const editor of window.visibleTextEditors) {
       editor.setDecorations(typ, [])
     }
     const i = context.subscriptions.indexOf(typ)
@@ -145,7 +145,7 @@
 
   /* update editors */
 
-  for (const editor of vscode.window.visibleTextEditors) {
+  for (const editor of window.visibleTextEditors) {
     update_editor(editor)
   }
 }
@@ -179,7 +179,7 @@
     document.set(decoration.type, content)
     document_decorations.set(uri, document)
 
-    for (const editor of vscode.window.visibleTextEditors) {
+    for (const editor of window.visibleTextEditors) {
       if (uri === editor.document.uri.toString()) {
         editor.setDecorations(typ, content)
       }
@@ -207,7 +207,7 @@
 function update_touched_documents()
 {
   const touched_editors: TextEditor[] = []
-  for (const editor of vscode.window.visibleTextEditors) {
+  for (const editor of window.visibleTextEditors) {
     if (touched_documents.has(editor.document)) {
       touched_editors.push(editor)
     }
diff -r 44e703278dfd -r 1f93eb5c3d77 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Tue May 30 11:50:12 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Tue May 30 11:54:53 2017 +0200
@@ -1,6 +1,6 @@
 'use strict';
 
-import * as vscode from 'vscode';
+import { ExtensionContext, workspace, window } from 'vscode';
 import * as path from 'path';
 import * as fs from 'fs';
 import * as os from 'os';
@@ -14,7 +14,7 @@
 
 let last_caret_update: protocol.Caret_Update = {}
 
-export function activate(context: vscode.ExtensionContext)
+export function activate(context: ExtensionContext)
 {
   const is_windows = os.type().startsWith("Windows")
 
@@ -26,7 +26,7 @@
   /* server */
 
   if (isabelle_home === "")
-    vscode.window.showErrorMessage("Missing user settings: isabelle.home")
+    window.showErrorMessage("Missing user settings: isabelle.home")
   else {
     const isabelle_tool = isabelle_home + "/bin/isabelle"
     const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
@@ -49,10 +49,10 @@
     /* decorations */
 
     decorations.init(context)
-    vscode.workspace.onDidChangeConfiguration(() => decorations.init(context))
-    vscode.workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document))
-    vscode.window.onDidChangeActiveTextEditor(decorations.update_editor)
-    vscode.workspace.onDidCloseTextDocument(decorations.close_document)
+    workspace.onDidChangeConfiguration(() => decorations.init(context))
+    workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document))
+    window.onDidChangeActiveTextEditor(decorations.update_editor)
+    workspace.onDidCloseTextDocument(decorations.close_document)
 
     client.onReady().then(() =>
       client.onNotification(protocol.decoration_type, decorations.apply_decoration))
@@ -60,14 +60,14 @@
 
     /* caret handling and dynamic output */
 
-    const dynamic_output = vscode.window.createOutputChannel("Isabelle Output")
+    const dynamic_output = window.createOutputChannel("Isabelle Output")
     context.subscriptions.push(dynamic_output)
     dynamic_output.show(true)
     dynamic_output.hide()
 
     function update_caret()
     {
-      const editor = vscode.window.activeTextEditor
+      const editor = window.activeTextEditor
       let caret_update: protocol.Caret_Update = {}
       if (editor) {
         const uri = editor.document.uri
@@ -86,8 +86,8 @@
     {
       client.onNotification(protocol.dynamic_output_type,
         params => { dynamic_output.clear(); dynamic_output.appendLine(params.body) })
-      vscode.window.onDidChangeActiveTextEditor(_ => update_caret())
-      vscode.window.onDidChangeTextEditorSelection(_ => update_caret())
+      window.onDidChangeActiveTextEditor(_ => update_caret())
+      window.onDidChangeTextEditorSelection(_ => update_caret())
       update_caret()
     })