# HG changeset patch # User wenzelm # Date 1496090983 -7200 # Node ID 7f87310d6c092550f148a617c82c9a6cb94015a1 # Parent 38fbf13f79867f043bf8b368f20d6c742f5edd7f update preview after document change; clarified encode_name/decode_name; clarified other_column; diff -r 38fbf13f7986 -r 7f87310d6c09 src/Tools/VSCode/extension/src/preview.ts --- a/src/Tools/VSCode/extension/src/preview.ts Mon May 29 19:50:46 2017 +0200 +++ b/src/Tools/VSCode/extension/src/preview.ts Mon May 29 22:49:43 2017 +0200 @@ -1,7 +1,7 @@ 'use strict'; -import { TextDocumentContentProvider, ExtensionContext, Uri, Position, ViewColumn, - workspace, window, commands } from 'vscode' +import { TextDocumentContentProvider, ExtensionContext, Event, EventEmitter, Uri, Position, + ViewColumn, workspace, window, commands } from 'vscode' const uri_scheme = 'isabelle-preview'; @@ -9,12 +9,31 @@ class Provider implements TextDocumentContentProvider { constructor() { } - dispose() { } - provideTextDocumentContent(uri: Uri): string | Thenable + private emitter = new EventEmitter() + private waiting: boolean = false; + + get onDidChange(): Event { return this.emitter.event } + + public update(document_uri: Uri) { - const [name, pos] = decode_location(uri) + if (!this.waiting) { + this.waiting = true + setTimeout(() => + { + this.waiting = false + this.emitter.fire(encode_name(document_uri)) + }, 300) + } + } + + provideTextDocumentContent(preview_uri: Uri): string | Thenable + { + const document_uri = decode_name(preview_uri) + const editor = + window.visibleTextEditors.find(editor => + document_uri.toString() === editor.document.uri.toString()) return ` @@ -22,49 +41,53 @@

Isabelle Preview

${JSON.stringify([name, pos])}

file = ${document_uri.fsPath}
line count = ${editor.document.lineCount}

` } } -export function encode_location(uri: Uri, pos: Position): Uri +export function encode_name(document_uri: Uri): Uri { - const query = JSON.stringify([uri.toString(), pos.line, pos.character]) - return Uri.parse(uri_scheme + ":Preview?" + query) + return Uri.parse(uri_scheme + ":Preview?" + JSON.stringify([document_uri.toString()])) } -export function decode_location(uri: Uri): [Uri, Position] +export function decode_name(preview_uri: Uri): Uri { - let [name, line, character] = <[string, number, number]>JSON.parse(uri.query) - return [Uri.parse(name), new Position(line, character)] + const [name] = <[string]>JSON.parse(preview_uri.query) + return Uri.parse(name) } -function view_column(side_by_side: boolean = true): ViewColumn | undefined +function other_column(): ViewColumn { const active = window.activeTextEditor - if (!active) { return ViewColumn.One } - if (!side_by_side) { return active.viewColumn } - - if (active.viewColumn == ViewColumn.One) return ViewColumn.Two - else if (active.viewColumn == ViewColumn.Two) return ViewColumn.Three - else return ViewColumn.One + if (!active || active.viewColumn === ViewColumn.Three) return ViewColumn.One + else if (active.viewColumn === ViewColumn.One) return ViewColumn.Two + else return ViewColumn.Three } export function init(context: ExtensionContext) { const provider = new Provider() + context.subscriptions.push(workspace.registerTextDocumentContentProvider(uri_scheme, provider)) + context.subscriptions.push(provider) - const provider_registration = - workspace.registerTextDocumentContentProvider(uri_scheme, provider) - - const command_registration = + context.subscriptions.push( commands.registerTextEditorCommand("isabelle.preview", editor => { - const uri = encode_location(editor.document.uri, editor.selection.active) - return workspace.openTextDocument(uri).then(doc => - commands.executeCommand("vscode.previewHtml", uri, view_column(), "Isabelle Preview")) - }) + const preview_uri = encode_name(editor.document.uri) + return workspace.openTextDocument(preview_uri).then(doc => + commands.executeCommand("vscode.previewHtml", preview_uri, other_column(), "Isabelle Preview")) + })) - context.subscriptions.push(provider, provider_registration, command_registration) + context.subscriptions.push( + workspace.onDidChangeTextDocument(event => + { + if (event.document.languageId === 'isabelle') { + provider.update(event.document.uri) + } + })) }