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