# HG changeset patch # User wenzelm # Date 1582654821 -3600 # Node ID fe1b19bf5feffb3beae5b2e60d23cef7dddc4623 # Parent be84312a2d5362f2904f1d85b6b314ce2e03ce59 removed duplicate (amending 5763d9a2f47d, 5aa9cb83e70e); diff -r be84312a2d53 -r fe1b19bf5fef src/Tools/VSCode/extension/src/preview.ts --- a/src/Tools/VSCode/extension/src/preview.ts Tue Feb 25 18:30:08 2020 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,97 +0,0 @@ -'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 = - 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") -}