# HG changeset patch
# User wenzelm
# Date 1582727884 -3600
# Node ID 6aa2dc2639127a4d00e1e59b602f89b438949a11
# Parent  5c0293826dc8601c76e6a914a92d5c11efb09bc8
less ambitious preview: discontinued preview-update / preview-source which did not work on the spot via WebviewPanel;

diff -r 5c0293826dc8 -r 6aa2dc263912 src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Wed Feb 26 15:34:52 2020 +0100
+++ b/src/Tools/VSCode/extension/package.json	Wed Feb 26 15:38:04 2020 +0100
@@ -27,8 +27,7 @@
         "onLanguage:isabelle-ml",
         "onLanguage:bibtex",
         "onCommand:isabelle.preview",
-        "onCommand:isabelle.preview-split",
-        "onCommand:isabelle.preview-source"
+        "onCommand:isabelle.preview-split"
     ],
     "main": "./out/src/extension",
     "contributes": {
@@ -48,15 +47,6 @@
                 }
             },
             {
-                "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",
@@ -66,15 +56,6 @@
                 }
             },
             {
-                "command": "isabelle.preview-source",
-                "title": "Show Source",
-                "category": "Isabelle",
-                "icon": {
-                    "light": "./media/ViewSource.svg",
-                    "dark": "./media/ViewSource_inverse.svg"
-                }
-            },
-            {
                 "command": "isabelle.include-word",
                 "title": "Include word",
                 "category": "Isabelle"
@@ -131,16 +112,6 @@
                     "when": "editorLangId == bibtex",
                     "command": "isabelle.preview-split",
                     "group": "navigation"
-                },
-                {
-                    "when": "resourceScheme == isabelle-preview",
-                    "command": "isabelle.preview-update",
-                    "group": "navigation"
-                },
-                {
-                    "when": "resourceScheme == isabelle-preview",
-                    "command": "isabelle.preview-source",
-                    "group": "navigation"
                 }
             ],
             "explorer/context": [
diff -r 5c0293826dc8 -r 6aa2dc263912 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Wed Feb 26 15:34:52 2020 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed Feb 26 15:38:04 2020 +0100
@@ -139,9 +139,7 @@
 
     context.subscriptions.push(
       commands.registerCommand("isabelle.preview", uri => preview_panel.request(uri, false)),
-      commands.registerCommand("isabelle.preview-split", uri => preview_panel.request(uri, true)),
-      commands.registerCommand("isabelle.preview-source", preview_panel.source),
-      commands.registerCommand("isabelle.preview-update", preview_panel.update))
+      commands.registerCommand("isabelle.preview-split", uri => preview_panel.request(uri, true)))
 
     language_client.onReady().then(() => preview_panel.setup(context, language_client))
 
diff -r 5c0293826dc8 -r 6aa2dc263912 src/Tools/VSCode/extension/src/preview_panel.ts
--- a/src/Tools/VSCode/extension/src/preview_panel.ts	Wed Feb 26 15:34:52 2020 +0100
+++ b/src/Tools/VSCode/extension/src/preview_panel.ts	Wed Feb 26 15:38:04 2020 +0100
@@ -1,94 +1,59 @@
 'use strict';
 
-import * as timers from 'timers'
-import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider,
-  ExtensionContext, Event, EventEmitter, Uri, Position, workspace,
-  window, commands, WebviewPanel } from 'vscode'
+import { ExtensionContext, Uri, workspace,
+  window, commands, ViewColumn, WebviewPanel } from 'vscode'
 import { LanguageClient } from 'vscode-languageclient';
 import * as library from './library'
 import * as protocol from './protocol'
-import { Content_Provider } from './content_provider'
 
 
-/* HTML content */
-
-const content_provider = new Content_Provider("isabelle-preview")
-
-function encode_preview(document_uri: Uri | undefined): Uri | undefined
-{
-  if (document_uri && library.is_file(document_uri)) {
-    return content_provider.uri_template.with({ query: document_uri.fsPath })
-  }
-  else undefined
-}
-
-function decode_preview(preview_uri: Uri | undefined): Uri | undefined
-{
-  if (preview_uri && preview_uri.scheme === content_provider.uri_scheme) {
-    return Uri.file(preview_uri.query)
-  }
-  else undefined
-}
-
-
-/* setup */
-
 let language_client: LanguageClient
 
+class Panel
+{
+  private webview_panel: WebviewPanel
+
+  public set_content(title: string, body: string)
+  {
+    this.webview_panel.title = title
+    this.webview_panel.webview.html = body
+  }
+
+  public reveal(column: ViewColumn)
+  {
+    this.webview_panel.reveal(column)
+  }
+
+  constructor(column: ViewColumn)
+  {
+    this.webview_panel =
+      window.createWebviewPanel("isabelle-preview", "Preview", column,
+        {
+          enableScripts: true
+        });
+    this.webview_panel.onDidDispose(() => { panel = null })
+  }
+}
+
+let panel: Panel
+
 export function setup(context: ExtensionContext, client: LanguageClient)
 {
-  context.subscriptions.push(content_provider.register())
-
-  var panel: WebviewPanel
   language_client = client
   language_client.onNotification(protocol.preview_response_type, params =>
     {
-      const preview_uri = encode_preview(Uri.parse(params.uri))
-      if (!panel) {
-        panel = window.createWebviewPanel(
-          preview_uri.fsPath,
-          params.label,
-          params.column,
-          {
-            enableScripts: true,
-            retainContextWhenHidden: true
-          }
-        );
-      }
-      panel.webview.html = params.content;
+      if (!panel) { panel = new Panel(params.column) }
+      else panel.reveal(params.column)
+      panel.set_content(params.label, params.content)
     })
 }
 
-
-/* commands */
-
 export function request(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) {
+  if (language_client) {
     language_client.sendNotification(protocol.preview_request_type,
       { uri: document_uri.toString(),
         column: library.adjacent_editor_column(window.activeTextEditor, split) })
   }
 }
-
-export function update(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 source(preview_uri: Uri)
-{
-  const document_uri = decode_preview(preview_uri)
-  if (document_uri) {
-    const editor = library.find_file_editor(document_uri)
-    if (editor) window.showTextDocument(editor.document, editor.viewColumn)
-    else workspace.openTextDocument(document_uri).then(window.showTextDocument)
-  }
-  else commands.executeCommand("workbench.action.navigateBack")
-}