# HG changeset patch
# User wenzelm
# Date 1496256239 -7200
# Node ID 44e44bfc738a98b7dd527ebeedeee99e92fbbd67
# Parent  d2b2f08533c50ae3ef8bcb3ef420b0e794a95a20
tuned signature;
tuned;

diff -r d2b2f08533c5 -r 44e44bfc738a src/Tools/VSCode/extension/src/extension.ts
--- 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))
 
diff -r d2b2f08533c5 -r 44e44bfc738a src/Tools/VSCode/extension/src/preview.ts
--- a/src/Tools/VSCode/extension/src/preview.ts	Wed May 31 20:33:26 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts	Wed May 31 20:43:59 2017 +0200
@@ -74,8 +74,15 @@
     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))
+  language_client.onNotification(protocol.preview_response_type, params =>
+    {
+      const preview_uri = encode_preview(Uri.parse(params.uri))
+      if (preview_uri) {
+        preview_content.set(preview_uri.toString(), params.content)
+        if (params.column == 0) content_provider.update(preview_uri)
+        else commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label)
+      }
+    })
 }
 
 
@@ -91,16 +98,7 @@
   else return ViewColumn.Three
 }
 
-export function update_preview(preview_uri: Uri)
-{
-  const document_uri = decode_preview(preview_uri)
-  if (document_uri && language_client) {
-    language_client.sendNotification(protocol.preview_request_type,
-      { uri: document_uri.toString(), column: 0 })
-  }
-}
-
-export function request_preview(uri?: Uri, split: boolean = false)
+export function request(uri?: Uri, split: boolean = false)
 {
   const document_uri = uri || window.activeTextEditor.document.uri
   const preview_uri = encode_preview(document_uri)
@@ -110,17 +108,16 @@
   }
 }
 
-export function show_preview(document_uri: Uri, column: number, label: string, content: string)
+export function update(preview_uri: Uri)
 {
-  const preview_uri = encode_preview(document_uri)
-  if (preview_uri && content_provider) {
-    preview_content.set(preview_uri.toString(), content)
-    if (column == 0) content_provider.update(preview_uri)
-    else commands.executeCommand("vscode.previewHtml", preview_uri, column, label)
+  const document_uri = decode_preview(preview_uri)
+  if (document_uri && language_client) {
+    language_client.sendNotification(protocol.preview_request_type,
+      { uri: document_uri.toString(), column: 0 })
   }
 }
 
-export function show_source(preview_uri: Uri)
+export function source(preview_uri: Uri)
 {
   const document_uri = decode_preview(preview_uri)
   if (document_uri) {