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