# HG changeset patch
# User wenzelm
# Date 1496244721 -7200
# Node ID 8e6a833da7dbf6ba9fc1efa9ad7cd2138a399e51
# Parent  d8c5603c17327dcade187da07f96520def713594
register commands earlier, before prover startup;

diff -r d8c5603c1732 -r 8e6a833da7db src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Wed May 31 17:25:26 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed May 31 17:32:01 2017 +0200
@@ -1,12 +1,12 @@
 'use strict';
 
-import { ExtensionContext, workspace, window } from 'vscode';
 import * as path from 'path';
 import * as fs from 'fs';
 import * as library from './library'
 import * as decorations from './decorations';
 import * as preview from './preview';
 import * as protocol from './protocol';
+import { ExtensionContext, workspace, window, commands } from 'vscode';
 import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType }
   from 'vscode-languageclient';
 
@@ -101,6 +101,11 @@
 
     /* preview */
 
+    context.subscriptions.push(
+      commands.registerCommand("isabelle.preview", uri => preview.request_preview(uri, false)),
+      commands.registerCommand("isabelle.preview-side", uri => preview.request_preview(uri, true)),
+      commands.registerCommand("isabelle.preview-source", preview.show_source))
+
     language_client.onReady().then(() => preview.init(context, language_client))
 
 
diff -r d8c5603c1732 -r 8e6a833da7db src/Tools/VSCode/extension/src/preview.ts
--- a/src/Tools/VSCode/extension/src/preview.ts	Wed May 31 17:25:26 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts	Wed May 31 17:32:01 2017 +0200
@@ -45,7 +45,7 @@
   </body>
   </html>`
 
-class Provider implements TextDocumentContentProvider
+class Content_Provider implements TextDocumentContentProvider
 {
   dispose() { }
 
@@ -63,21 +63,16 @@
 /* init */
 
 let language_client: LanguageClient
-let provider: Provider
+let content_provider: Content_Provider
 
 export function init(context: ExtensionContext, client: LanguageClient)
 {
   language_client = client
 
-  provider = new Provider()
+  content_provider = new Content_Provider()
   context.subscriptions.push(
-    workspace.registerTextDocumentContentProvider(preview_uri_scheme, provider),
-    provider)
-
-  context.subscriptions.push(
-    commands.registerCommand("isabelle.preview", uri => request_preview(uri, false)),
-    commands.registerCommand("isabelle.preview-side", uri => request_preview(uri, true)),
-    commands.registerCommand("isabelle.preview-source", show_source))
+    workspace.registerTextDocumentContentProvider(preview_uri_scheme, content_provider),
+    content_provider)
 
   language_client.onNotification(protocol.preview_response_type,
     params => show_preview(Uri.parse(params.uri), params.column, params.label, params.content))
@@ -96,26 +91,26 @@
   else return ViewColumn.Three
 }
 
-function request_preview(uri?: Uri, side: boolean = false)
+export function request_preview(uri?: Uri, side: boolean = false)
 {
   const document_uri = uri || window.activeTextEditor.document.uri
   const preview_uri = encode_preview(document_uri)
-  if (preview_uri) {
+  if (preview_uri && language_client) {
     language_client.sendNotification(protocol.preview_request_type,
       {uri: document_uri.toString(), column: preview_column(side) })
   }
 }
 
-function show_preview(document_uri: Uri, column: ViewColumn, label: string, content: string)
+export function show_preview(document_uri: Uri, column: ViewColumn, label: string, content: string)
 {
   const preview_uri = encode_preview(document_uri)
-  if (preview_uri) {
+  if (preview_uri && content_provider) {
     preview_content.set(preview_uri.toString(), content)
     commands.executeCommand("vscode.previewHtml", preview_uri, column, label)
   }
 }
 
-function show_source(preview_uri: Uri)
+export function show_source(preview_uri: Uri)
 {
   const document_uri = decode_preview(preview_uri)
   if (document_uri) {