--- 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
{
--- 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)
})
--- 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())
--- 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)