src/Tools/VSCode/extension/src/preview_panel.ts

update to WebviewPanel API, following initial version by Peter Zeller;

'use strict';

import * as timers from 'timers'
import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider,
  ExtensionContext, Event, EventEmitter, Uri, Position, workspace,
  window, commands, 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

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;
    })
}


/* 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 = 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")
}