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