--- a/src/Tools/VSCode/extension/src/extension.ts Wed May 31 20:33:26 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts Wed May 31 20:43:59 2017 +0200
@@ -102,10 +102,10 @@
/* preview */
context.subscriptions.push(
- commands.registerCommand("isabelle.preview", uri => preview.request_preview(uri, false)),
- commands.registerCommand("isabelle.preview-split", uri => preview.request_preview(uri, true)),
- commands.registerCommand("isabelle.preview-source", preview.show_source),
- commands.registerCommand("isabelle.preview-update", preview.update_preview))
+ commands.registerCommand("isabelle.preview", uri => preview.request(uri, false)),
+ commands.registerCommand("isabelle.preview-split", uri => preview.request(uri, true)),
+ commands.registerCommand("isabelle.preview-source", preview.source),
+ commands.registerCommand("isabelle.preview-update", preview.update))
language_client.onReady().then(() => preview.init(context, language_client))