# HG changeset patch
# User wenzelm
# Date 1496255606 -7200
# Node ID d2b2f08533c50ae3ef8bcb3ef420b0e794a95a20
# Parent  1be7135917a604abd713847ca1f265ff66ca9d51
added update operation;

diff -r 1be7135917a6 -r d2b2f08533c5 src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Wed May 31 20:13:05 2017 +0200
+++ b/src/Tools/VSCode/extension/package.json	Wed May 31 20:33:26 2017 +0200
@@ -36,6 +36,15 @@
                 }
             },
             {
+                "command": "isabelle.preview-update",
+                "title": "Update Preview",
+                "category": "Isabelle",
+                "icon": {
+                    "light": "./media/Preview.svg",
+                    "dark": "./media/Preview_inverse.svg"
+                }
+            },
+            {
                 "command": "isabelle.preview-split",
                 "title": "Open Preview (Split Editor)",
                 "category": "Isabelle",
@@ -64,6 +73,11 @@
                 },
                 {
                     "when": "resourceScheme == isabelle-preview",
+                    "command": "isabelle.preview-update",
+                    "group": "navigation"
+                },
+                {
+                    "when": "resourceScheme == isabelle-preview",
                     "command": "isabelle.preview-source",
                     "group": "navigation"
                 }
diff -r 1be7135917a6 -r d2b2f08533c5 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Wed May 31 20:13:05 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed May 31 20:33:26 2017 +0200
@@ -104,14 +104,15 @@
     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-source", preview.show_source),
+      commands.registerCommand("isabelle.preview-update", preview.update_preview))
 
     language_client.onReady().then(() => preview.init(context, language_client))
 
 
     /* start server */
 
-    context.subscriptions.push(language_client.start());
+    context.subscriptions.push(language_client.start())
   }
 }
 
diff -r 1be7135917a6 -r d2b2f08533c5 src/Tools/VSCode/extension/src/preview.ts
--- a/src/Tools/VSCode/extension/src/preview.ts	Wed May 31 20:13:05 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts	Wed May 31 20:33:26 2017 +0200
@@ -91,22 +91,32 @@
   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)
 {
   const document_uri = uri || window.activeTextEditor.document.uri
   const preview_uri = encode_preview(document_uri)
   if (preview_uri && language_client) {
     language_client.sendNotification(protocol.preview_request_type,
-      {uri: document_uri.toString(), column: preview_column(split) })
+      { uri: document_uri.toString(), column: preview_column(split) })
   }
 }
 
-export function show_preview(document_uri: Uri, column: ViewColumn, label: string, content: string)
+export function show_preview(document_uri: Uri, column: number, label: string, content: string)
 {
   const preview_uri = encode_preview(document_uri)
   if (preview_uri && content_provider) {
     preview_content.set(preview_uri.toString(), content)
-    commands.executeCommand("vscode.previewHtml", preview_uri, column, label)
+    if (column == 0) content_provider.update(preview_uri)
+    else commands.executeCommand("vscode.previewHtml", preview_uri, column, label)
   }
 }