--- a/src/Tools/VSCode/extension/package.json Mon May 29 16:40:56 2017 +0200
+++ b/src/Tools/VSCode/extension/package.json Mon May 29 22:49:52 2017 +0200
@@ -22,6 +22,12 @@
],
"main": "./out/src/extension",
"contributes": {
+ "commands": [
+ {
+ "command": "isabelle.preview",
+ "title": "Isabelle Document Preview"
+ }
+ ],
"languages": [
{
"id": "isabelle",
--- a/src/Tools/VSCode/extension/src/extension.ts Mon May 29 16:40:56 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts Mon May 29 22:49:52 2017 +0200
@@ -5,6 +5,7 @@
import * as fs from 'fs';
import * as os from 'os';
import * as decorations from './decorations';
+import * as preview from './preview';
import * as protocol from './protocol';
import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType }
from 'vscode-languageclient';
@@ -106,6 +107,11 @@
})
+ /* preview */
+
+ preview.init(context)
+
+
/* start server */
context.subscriptions.push(client.start());
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/preview.ts Mon May 29 22:49:52 2017 +0200
@@ -0,0 +1,93 @@
+'use strict';
+
+import { TextDocumentContentProvider, ExtensionContext, Event, EventEmitter, Uri, Position,
+ ViewColumn, workspace, window, commands } from 'vscode'
+
+
+const uri_scheme = 'isabelle-preview';
+
+class Provider implements TextDocumentContentProvider
+{
+ constructor() { }
+ dispose() { }
+
+ private emitter = new EventEmitter<Uri>()
+ private waiting: boolean = false;
+
+ get onDidChange(): Event<Uri> { return this.emitter.event }
+
+ public update(document_uri: 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<string>
+ {
+ const document_uri = decode_name(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>`
+ }
+}
+
+export function encode_name(document_uri: Uri): Uri
+{
+ return Uri.parse(uri_scheme + ":Preview?" + JSON.stringify([document_uri.toString()]))
+}
+
+export function decode_name(preview_uri: Uri): Uri
+{
+ const [name] = <[string]>JSON.parse(preview_uri.query)
+ return Uri.parse(name)
+}
+
+function other_column(): ViewColumn
+{
+ const active = window.activeTextEditor
+ 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)
+
+ context.subscriptions.push(
+ commands.registerTextEditorCommand("isabelle.preview", editor =>
+ {
+ 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(
+ workspace.onDidChangeTextDocument(event =>
+ {
+ if (event.document.languageId === 'isabelle') {
+ provider.update(event.document.uri)
+ }
+ }))
+}