# HG changeset patch # User wenzelm # Date 1582662486 -3600 # Node ID 7a867a38712a283e75ec35e9ab12145fd28b56f7 # Parent fe1b19bf5feffb3beae5b2e60d23cef7dddc4623 clarified Panel; discontinued intermediate Content_Provider; diff -r fe1b19bf5fef -r 7a867a38712a src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Tue Feb 25 19:20:21 2020 +0100 +++ b/src/Tools/VSCode/extension/src/extension.ts Tue Feb 25 21:28:06 2020 +0100 @@ -133,8 +133,7 @@ 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-auto-update", state_panel.auto_update)) language_client.onReady().then(() => state_panel.setup(context, language_client)) diff -r fe1b19bf5fef -r 7a867a38712a src/Tools/VSCode/extension/src/state_panel.ts --- a/src/Tools/VSCode/extension/src/state_panel.ts Tue Feb 25 19:20:21 2020 +0100 +++ b/src/Tools/VSCode/extension/src/state_panel.ts Tue Feb 25 21:28:06 2020 +0100 @@ -4,88 +4,98 @@ import * as protocol from './protocol' import { Content_Provider } from './content_provider' import { LanguageClient, VersionedTextDocumentIdentifier } from 'vscode-languageclient'; -import { Uri, ExtensionContext, workspace, commands, window, Webview, WebviewPanel } from 'vscode' +import { Uri, ExtensionContext, workspace, commands, window, Webview, WebviewPanel, ViewColumn } from 'vscode' +import { create } from 'domain'; -/* HTML content */ +let language_client: LanguageClient -const content_provider = new Content_Provider("isabelle-state") - -function encode_state(id: number | undefined): Uri | undefined +class Panel { - return id ? content_provider.uri_template.with({ fragment: id.toString() }) : undefined -} + 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, html: string) + { + this.state_id = id + this.webview_panel.webview.html = html + } -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 + constructor(column: ViewColumn) + { + this.webview_panel = + window.createWebviewPanel("isabelle-state", "State", column, + { + enableScripts: true, + enableCommandUris: true, + retainContextWhenHidden: true, + }); + this.webview_panel.onDidDispose(exit_panel) } - else undefined + + public locate() + { + language_client.sendNotification(protocol.state_locate_type, { id: this.state_id }) + } + + public update() + { + language_client.sendNotification(protocol.state_update_type, { id: this.state_id }) + } + + public auto_update(enabled: boolean) + { + language_client.sendNotification( + protocol.state_auto_update_type, { id: this.state_id, enabled: enabled }) + } } -/* setup */ +/* global panel */ + +let panel: Panel -let language_client: LanguageClient +function check_panel(id: number): boolean +{ + return panel && panel.check_id(id) +} + +function exit_panel() +{ + if (panel) { + language_client.sendNotification(protocol.state_exit_type, { id: panel.get_id() }) + panel = null + } +} export function setup(context: ExtensionContext, client: LanguageClient) { - context.subscriptions.push(content_provider.register()) - - var panel: WebviewPanel language_client = client language_client.onNotification(protocol.state_output_type, params => { - const uri = encode_state(params.id) if (!panel) { const column = library.adjacent_editor_column(window.activeTextEditor, true) - panel = window.createWebviewPanel( - uri.fsPath, - "State", - column, - { - enableScripts: true, - retainContextWhenHidden: true - } - ); + panel = new Panel(column) } - panel.webview.html = params.content; + 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 init(uri: Uri) { + language_client.sendNotification(protocol.state_init_type) } -export function exit_uri(uri: Uri) -{ - const id = decode_state(uri) - if (id) exit(id) -} +export function locate(id: number) { if (check_panel(id)) panel.locate() } -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 update(id: number) { if (check_panel(id)) panel.update() } export function auto_update(id: number, enabled: boolean) { - if (language_client) - language_client.sendNotification(protocol.state_auto_update_type, { id: id, enabled: enabled }) + if (check_panel(id)) { panel.auto_update(enabled) } }