--- a/src/Tools/VSCode/extension/src/preview.ts Tue May 30 21:38:38 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts Tue May 30 22:06:39 2017 +0200
@@ -6,49 +6,39 @@
import * as library from './library'
-/* generated content */
+/* HTML content */
-const uri_scheme = 'isabelle-preview';
+const preview_uri = Uri.parse("isabelle-preview:Preview")
-export function encode_preview(document_uri: Uri): Uri
-{
- return Uri.parse(uri_scheme + ":Preview?" + JSON.stringify([document_uri.toString()]))
-}
+const default_preview_content =
+ `<html>
+ <head>
+ <meta http-equiv="Content-type" content="text/html; charset=UTF-8">
+ </head>
+ <body>
+ <h1>Isabelle Preview</h1>
+ </body>
+ </html>`
-export function decode_preview(preview_uri: Uri): Uri
-{
- const [name] = <[string]>JSON.parse(preview_uri.query)
- return Uri.parse(name)
-}
+let preview_content = default_preview_content
class Provider implements TextDocumentContentProvider
{
dispose() { }
private emitter = new EventEmitter<Uri>()
- public update(preview_uri: Uri) { this.emitter.fire(preview_uri) }
+ public update() { this.emitter.fire(preview_uri) }
get onDidChange(): Event<Uri> { return this.emitter.event }
- provideTextDocumentContent(preview_uri: Uri): string | Thenable<string>
- {
- const document_uri = decode_preview(preview_uri)
- const editor =
- window.visibleTextEditors.find(editor =>
- document_uri.toString() === editor.document.uri.toString())
- return `
- <html>
- <head>
- <meta http-equiv="Content-type" content="text/html; charset=UTF-8">
- </head>
- <body>
- <h1>Isabelle Preview</h1>
- <ul>
- <li><b>file</b> = <code>${document_uri.fsPath}</code></li>` +
- (editor ? `<li><b>line count</b> = ${editor.document.lineCount}</li>` : "") +
- `</ul>
- </body>
- </html>`
- }
+ provideTextDocumentContent(uri: Uri): string { return preview_content }
+}
+
+export function update(content: string)
+{
+ preview_content = content === "" ? default_preview_content : content
+ provider.update()
+ commands.executeCommand("vscode.previewHtml", preview_uri,
+ library.other_column(window.activeTextEditor), "Isabelle Preview")
}
@@ -59,39 +49,6 @@
export function init(context: ExtensionContext)
{
provider = new Provider()
- context.subscriptions.push(workspace.registerTextDocumentContentProvider(uri_scheme, provider))
+ context.subscriptions.push(workspace.registerTextDocumentContentProvider(preview_uri.scheme, provider))
context.subscriptions.push(provider)
-
- context.subscriptions.push(
- commands.registerTextEditorCommand("isabelle.preview", editor =>
- {
- const preview_uri = encode_preview(editor.document.uri)
- return workspace.openTextDocument(preview_uri).then(doc =>
- commands.executeCommand("vscode.previewHtml", preview_uri,
- library.other_column(window.activeTextEditor), "Isabelle Preview"))
- }))
}
-
-
-/* handle document changes */
-
-const touched_documents = new Set<TextDocument>()
-let touched_timer: NodeJS.Timer
-
-function update_touched_documents()
-{
- if (provider) {
- for (const document of touched_documents) {
- provider.update(encode_preview(document.uri))
- }
- }
-}
-
-export function touch_document(document: TextDocument)
-{
- if (library.is_file(document.uri) && document.languageId === 'isabelle') {
- if (touched_timer) timers.clearTimeout(touched_timer)
- touched_documents.add(document)
- touched_timer = timers.setTimeout(update_touched_documents, 300)
- }
-}