# HG changeset patch # User wenzelm # Date 1496090992 -7200 # Node ID d7bc93a467bdf16124444bf4622749999799ebe8 # Parent 558ba6b37f5c764b89c35963b28ffe6add9fd21f# Parent 7f87310d6c092550f148a617c82c9a6cb94015a1 merged diff -r 558ba6b37f5c -r d7bc93a467bd src/Tools/VSCode/extension/package.json --- 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", diff -r 558ba6b37f5c -r d7bc93a467bd src/Tools/VSCode/extension/src/extension.ts --- 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()); diff -r 558ba6b37f5c -r d7bc93a467bd src/Tools/VSCode/extension/src/preview.ts --- /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() + private waiting: boolean = false; + + get onDidChange(): Event { 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 + { + const document_uri = decode_name(preview_uri) + const editor = + window.visibleTextEditors.find(editor => + document_uri.toString() === editor.document.uri.toString()) + return ` + + + + + +

Isabelle Preview

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

+ + ` + } +} + +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) + } + })) +}