# HG changeset patch
# User wenzelm
# Date 1582729685 -3600
# Node ID 6de04d21c26b8d575e66a25dfc72d7060933b0b5
# Parent  c213d067e60f5f7012e3a45c44d8b3aa9dff3145# Parent  aa7b0a5e9fe3bf24266dc47ccb68cb06ebeda9ac
merged

diff -r c213d067e60f -r 6de04d21c26b CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Feb 26 12:21:48 2020 +0000
+++ b/CONTRIBUTORS	Wed Feb 26 16:08:05 2020 +0100
@@ -17,6 +17,9 @@
   Traytel
   Extension of lift_bnf to support quotient types.
 
+* November 2019: Peter Zeller, TU Kaiserslautern
+  Update of Isabelle/VSCode to WebviewPanel API.
+
 * October..December 2019: Makarius Wenzel
   Isabelle/Phabrictor server setup, including Linux platform support in
   Isabelle/Scala. Client-side tool "isabelle hg_setup".
diff -r c213d067e60f -r 6de04d21c26b NEWS
--- a/NEWS	Wed Feb 26 12:21:48 2020 +0000
+++ b/NEWS	Wed Feb 26 16:08:05 2020 +0100
@@ -65,6 +65,11 @@
 * Support more brackets: \<llangle> \<rrangle> (intended for implicit argument syntax).
 
 
+*** Isabelle/VSCode Prover IDE ***
+
+* Update to WebviewPanel API.
+
+
 *** HOL ***
 
 * Improvements of the 'lift_bnf' command:
diff -r c213d067e60f -r 6de04d21c26b src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Feb 26 12:21:48 2020 +0000
+++ b/src/Pure/build-jars	Wed Feb 26 16:08:05 2020 +0100
@@ -196,7 +196,6 @@
   src/Tools/VSCode/src/protocol.scala
   src/Tools/VSCode/src/server.scala
   src/Tools/VSCode/src/state_panel.scala
-  src/Tools/VSCode/src/vscode_javascript.scala
   src/Tools/VSCode/src/vscode_rendering.scala
   src/Tools/VSCode/src/vscode_resources.scala
   src/Tools/VSCode/src/vscode_spell_checker.scala
diff -r c213d067e60f -r 6de04d21c26b src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Wed Feb 26 12:21:48 2020 +0000
+++ b/src/Tools/VSCode/extension/package.json	Wed Feb 26 16:08:05 2020 +0100
@@ -10,25 +10,24 @@
         "document preparation"
     ],
     "icon": "isabelle.png",
-    "version": "1.1.2",
+    "version": "1.2.0",
     "publisher": "makarius",
     "license": "MIT",
     "repository": {
-        "url": "https://isabelle.in.tum.de/repos/isabelle"
+        "url": "https://isabelle-dev.sketis.net"
     },
     "engines": {
-        "vscode": "^1.8.0"
+        "vscode": "^1.32.0"
     },
     "categories": [
-        "Languages"
+        "Programming Languages"
     ],
     "activationEvents": [
         "onLanguage:isabelle",
         "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": [
@@ -317,7 +288,7 @@
         "@types/node": "^7.0.66",
         "mocha": "^3.5.3",
         "typescript": "^2.9.2",
-        "vscode": "^1.1.18"
+        "vscode": "^1.1.36"
     },
     "dependencies": {
         "vscode-languageclient": "~3.2.2"
diff -r c213d067e60f -r 6de04d21c26b src/Tools/VSCode/extension/src/content_provider.ts
--- a/src/Tools/VSCode/extension/src/content_provider.ts	Wed Feb 26 12:21:48 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-'use strict'
-
-import { Event, EventEmitter, Uri, TextDocumentContentProvider, Disposable,
-  workspace } from 'vscode'
-
-
-export class Content_Provider implements TextDocumentContentProvider
-{
-  private _uri_template: Uri
-  get uri_template(): Uri { return this._uri_template }
-  get uri_scheme(): string { return this.uri_template.scheme }
-
-  constructor(uri_scheme: string)
-  {
-    this._uri_template = Uri.parse("scheme:").with({ scheme: uri_scheme })
-  }
-  dispose() { }
-
-  private emitter = new EventEmitter<Uri>()
-  public update(uri: Uri) { this.emitter.fire(uri) }
-  get onDidChange(): Event<Uri> { return this.emitter.event }
-
-  private content = new Map<string, string>()
-  public set_content(uri: Uri, content: string) { this.content.set(uri.toString(), content)}
-
-  provideTextDocumentContent(uri: Uri): string
-  {
-    return this.content.get(uri.toString()) || ""
-  }
-
-  public register(): Disposable
-  {
-    return workspace.registerTextDocumentContentProvider(this.uri_scheme, this)
-  }
-}
diff -r c213d067e60f -r 6de04d21c26b src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Wed Feb 26 12:21:48 2020 +0000
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed Feb 26 16:08:05 2020 +0100
@@ -130,11 +130,7 @@
     /* state panel */
 
     context.subscriptions.push(
-      commands.registerCommand("isabelle.state", uri => state_panel.init(uri)),
-      commands.registerCommand("_isabelle.state-locate", state_panel.locate),
-      commands.registerCommand("_isabelle.state-update", state_panel.update),
-      commands.registerCommand("_isabelle.state-auto-update", state_panel.auto_update),
-      workspace.onDidCloseTextDocument(document => state_panel.exit_uri(document.uri)))
+      commands.registerCommand("isabelle.state", uri => state_panel.init(uri)))
 
     language_client.onReady().then(() => state_panel.setup(context, language_client))
 
@@ -143,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 c213d067e60f -r 6de04d21c26b src/Tools/VSCode/extension/src/preview.ts
--- a/src/Tools/VSCode/extension/src/preview.ts	Wed Feb 26 12:21:48 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-'use strict';
-
-import * as timers from 'timers'
-import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider,
-  ExtensionContext, Event, EventEmitter, Uri, Position, workspace,
-  window, commands } 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
-
-export function setup(context: ExtensionContext, client: LanguageClient)
-{
-  context.subscriptions.push(content_provider.register())
-
-  language_client = client
-  language_client.onNotification(protocol.preview_response_type, params =>
-    {
-      const preview_uri = encode_preview(Uri.parse(params.uri))
-      if (preview_uri) {
-        content_provider.set_content(preview_uri, params.content)
-        content_provider.update(preview_uri)
-
-        const existing_document =
-          workspace.textDocuments.find(document =>
-            document.uri.scheme === preview_uri.scheme &&
-            document.uri.query === preview_uri.query)
-        if (!existing_document && params.column != 0) {
-          commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label)
-        }
-      }
-    })
-}
-
-
-/* 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) {
-    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 =
-      window.visibleTextEditors.find(editor =>
-        library.is_file(editor.document.uri) &&
-        editor.document.uri.fsPath === document_uri.fsPath)
-    if (editor) window.showTextDocument(editor.document, editor.viewColumn)
-    else workspace.openTextDocument(document_uri).then(window.showTextDocument)
-  }
-  else commands.executeCommand("workbench.action.navigateBack")
-}
diff -r c213d067e60f -r 6de04d21c26b src/Tools/VSCode/extension/src/preview_panel.ts
--- a/src/Tools/VSCode/extension/src/preview_panel.ts	Wed Feb 26 12:21:48 2020 +0000
+++ b/src/Tools/VSCode/extension/src/preview_panel.ts	Wed Feb 26 16:08:05 2020 +0100
@@ -1,93 +1,59 @@
 'use strict';
 
-import * as timers from 'timers'
-import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider,
-  ExtensionContext, Event, EventEmitter, Uri, Position, workspace,
-  window, commands } 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())
-
   language_client = client
   language_client.onNotification(protocol.preview_response_type, params =>
     {
-      const preview_uri = encode_preview(Uri.parse(params.uri))
-      if (preview_uri) {
-        content_provider.set_content(preview_uri, params.content)
-        content_provider.update(preview_uri)
-
-        const existing_document =
-          workspace.textDocuments.find(document =>
-            document.uri.scheme === preview_uri.scheme &&
-            document.uri.query === preview_uri.query)
-        if (!existing_document && params.column != 0) {
-          commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label)
-        }
-      }
+      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")
-}
diff -r c213d067e60f -r 6de04d21c26b src/Tools/VSCode/extension/src/state_panel.ts
--- a/src/Tools/VSCode/extension/src/state_panel.ts	Wed Feb 26 12:21:48 2020 +0000
+++ b/src/Tools/VSCode/extension/src/state_panel.ts	Wed Feb 26 16:08:05 2020 +0100
@@ -2,89 +2,91 @@
 
 import * as library from './library'
 import * as protocol from './protocol'
-import { Content_Provider } from './content_provider'
 import { LanguageClient } from 'vscode-languageclient';
-import { Uri, ExtensionContext, workspace, commands, window } from 'vscode'
-
-
-/* HTML content */
-
-const content_provider = new Content_Provider("isabelle-state")
+import { Uri, ExtensionContext, window, WebviewPanel, ViewColumn } from 'vscode'
 
-function encode_state(id: number | undefined): Uri | undefined
-{
-  return id ? content_provider.uri_template.with({ fragment: id.toString() }) : undefined
-}
-
-function decode_state(uri: Uri | undefined): number | undefined
-{
-  if (uri && uri.scheme === content_provider.uri_scheme) {
-    const id = parseInt(uri.fragment)
-    return id ? id : undefined
-  }
-  else undefined
-}
-
-
-/* setup */
 
 let language_client: LanguageClient
 
+function panel_column(): ViewColumn
+{
+  return library.adjacent_editor_column(window.activeTextEditor, true)
+}
+
+class Panel
+{
+  private state_id: number
+  private webview_panel: WebviewPanel
+
+  public get_id(): number { return this.state_id }
+  public check_id(id: number): boolean { return this.state_id == id }
+
+  public set_content(id: number, body: string)
+  {
+    this.state_id = id
+    this.webview_panel.webview.html = body
+  }
+
+  public reveal()
+  {
+    this.webview_panel.reveal(panel_column())
+  }
+
+  constructor()
+  {
+    this.webview_panel =
+      window.createWebviewPanel("isabelle-state", "State", panel_column(),
+        {
+          enableScripts: true
+        });
+    this.webview_panel.onDidDispose(exit_panel)
+    this.webview_panel.webview.onDidReceiveMessage(message =>
+      {
+        switch (message.command) {
+          case 'auto_update':
+            language_client.sendNotification(
+              protocol.state_auto_update_type, { id: this.state_id, enabled: message.enabled })
+            break;
+
+          case 'update':
+            language_client.sendNotification(protocol.state_update_type, { id: this.state_id })
+            break;
+
+          case 'locate':
+            language_client.sendNotification(protocol.state_locate_type, { id: this.state_id })
+            break;
+
+          default:
+            break;
+        }
+      })
+  }
+}
+
+let panel: Panel
+
+function exit_panel()
+{
+  if (panel) {
+    language_client.sendNotification(protocol.state_exit_type, { id: panel.get_id() })
+    panel = null
+  }
+}
+
+export function init(uri: Uri)
+{
+  if (language_client) {
+    if (panel) panel.reveal()
+    else language_client.sendNotification(protocol.state_init_type)
+  }
+}
+
 export function setup(context: ExtensionContext, client: LanguageClient)
 {
-  context.subscriptions.push(content_provider.register())
-
   language_client = client
   language_client.onNotification(protocol.state_output_type, params =>
     {
-      const uri = encode_state(params.id)
-      if (uri) {
-        content_provider.set_content(uri, params.content)
-        content_provider.update(uri)
-
-        const existing_document =
-          workspace.textDocuments.find(document =>
-            document.uri.scheme === uri.scheme &&
-            document.uri.fragment === uri.fragment)
-        if (!existing_document) {
-          const column = library.adjacent_editor_column(window.activeTextEditor, true)
-          commands.executeCommand("vscode.previewHtml", uri, column, "State")
-        }
-      }
+      if (!panel) { panel = new Panel() }
+      panel.set_content(params.id, params.content)
     })
 }
-
-
-/* commands */
-
-export function init(uri: Uri)
-{
-  if (language_client) language_client.sendNotification(protocol.state_init_type)
-}
-
-export function exit(id: number)
-{
-  if (language_client) language_client.sendNotification(protocol.state_exit_type, { id: id })
-}
-
-export function exit_uri(uri: Uri)
-{
-  const id = decode_state(uri)
-  if (id) exit(id)
-}
-
-export function locate(id: number)
-{
-  if (language_client) language_client.sendNotification(protocol.state_locate_type, { id: id })
-}
-
-export function update(id: number)
-{
-  if (language_client) language_client.sendNotification(protocol.state_update_type, { id: id })
-}
-
-export function auto_update(id: number, enabled: boolean)
-{
-  if (language_client)
-    language_client.sendNotification(protocol.state_auto_update_type, { id: id, enabled: enabled })
-}
diff -r c213d067e60f -r 6de04d21c26b src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Wed Feb 26 12:21:48 2020 +0000
+++ b/src/Tools/VSCode/src/state_panel.scala	Wed Feb 26 16:08:05 2020 +0100
@@ -109,14 +109,17 @@
   /* controls */
 
   private def controls_script =
-    VSCode_JavaScript.invoke_command +
 """
+const vscode = acquireVsCodeApi();
+
 function invoke_auto_update(enabled)
-{ invoke_command("_isabelle.state-auto-update", [""" + id + """, enabled]) }
+{ vscode.postMessage({'command': 'auto_update', 'enabled': enabled}) }
 
-function invoke_update() { invoke_command("_isabelle.state-update", [""" + id + """]) }
+function invoke_update()
+{ vscode.postMessage({'command': 'update'}) }
 
-function invoke_locate() { invoke_command("_isabelle.state-locate", [""" + id + """]) }
+function invoke_locate()
+{ vscode.postMessage({'command': 'locate'}) }
 """
 
   private def auto_update_button: XML.Elem =
diff -r c213d067e60f -r 6de04d21c26b src/Tools/VSCode/src/vscode_javascript.scala
--- a/src/Tools/VSCode/src/vscode_javascript.scala	Wed Feb 26 12:21:48 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-/*  Title:      Tools/VSCode/src/vscode_javascript.scala
-    Author:     Makarius
-
-JavaScript snippets for VSCode HTML view.
-*/
-
-package isabelle.vscode
-
-
-import isabelle._
-
-
-object VSCode_JavaScript
-{
-  val invoke_command =
-"""
-function invoke_command(name, args)
-{
-  window.parent.postMessage(
-    {
-      command: "did-click-link",
-      data: "command:" + encodeURIComponent(name) + "?" + encodeURIComponent(JSON.stringify(args))
-    }, "file://")
-}
-"""
-}