# HG changeset patch
# User wenzelm
# Date 1497638676 -7200
# Node ID ee4c2d5b650ec5e15f405db193da5397ca3dd3b6
# Parent  6187612e83c134708c06656bf1472464ef69c239
tuned signature;

diff -r 6187612e83c1 -r ee4c2d5b650e src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Fri Jun 16 16:21:17 2017 +0200
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Fri Jun 16 20:44:36 2017 +0200
@@ -65,11 +65,11 @@
 ]
 
 
-/* init */
+/* setup */
 
 const types = new Map<string, TextEditorDecorationType>()
 
-export function init(context: ExtensionContext)
+export function setup(context: ExtensionContext)
 {
   function decoration(options: DecorationRenderOptions): TextEditorDecorationType
   {
diff -r 6187612e83c1 -r ee4c2d5b650e src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Fri Jun 16 16:21:17 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Fri Jun 16 20:44:36 2017 +0200
@@ -49,9 +49,9 @@
 
     /* decorations */
 
-    decorations.init(context)
+    decorations.setup(context)
     context.subscriptions.push(
-      workspace.onDidChangeConfiguration(() => decorations.init(context)),
+      workspace.onDidChangeConfiguration(() => decorations.setup(context)),
       workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document)),
       window.onDidChangeActiveTextEditor(decorations.update_editor),
       workspace.onDidCloseTextDocument(decorations.close_document))
@@ -120,7 +120,7 @@
       commands.registerCommand("isabelle.preview-source", preview.source),
       commands.registerCommand("isabelle.preview-update", preview.update))
 
-    language_client.onReady().then(() => preview.init(context, language_client))
+    language_client.onReady().then(() => preview.setup(context, language_client))
 
 
     /* Isabelle symbols */
@@ -128,7 +128,7 @@
     language_client.onReady().then(() =>
     {
       language_client.onNotification(protocol.symbols_type,
-        params => symbol.init(context, params.entries))
+        params => symbol.setup(context, params.entries))
       language_client.sendNotification(protocol.symbols_request_type)
     })
 
diff -r 6187612e83c1 -r ee4c2d5b650e src/Tools/VSCode/extension/src/preview.ts
--- a/src/Tools/VSCode/extension/src/preview.ts	Fri Jun 16 16:21:17 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts	Fri Jun 16 20:44:36 2017 +0200
@@ -31,11 +31,11 @@
 }
 
 
-/* init */
+/* setup */
 
 let language_client: LanguageClient
 
-export function init(context: ExtensionContext, client: LanguageClient)
+export function setup(context: ExtensionContext, client: LanguageClient)
 {
   context.subscriptions.push(content_provider.register())
 
diff -r 6187612e83c1 -r ee4c2d5b650e src/Tools/VSCode/extension/src/symbol.ts
--- a/src/Tools/VSCode/extension/src/symbol.ts	Fri Jun 16 16:21:17 2017 +0200
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Fri Jun 16 20:44:36 2017 +0200
@@ -113,7 +113,7 @@
   registerSubstitutions: (substitutions: LanguageEntry) => Disposable
 }
 
-export function init(context: ExtensionContext, entries: [Entry])
+export function setup(context: ExtensionContext, entries: [Entry])
 {
   update_entries(entries)