# HG changeset patch # User wenzelm # Date 1496080246 -7200 # Node ID 38fbf13f79867f043bf8b368f20d6c742f5edd7f # Parent 47309113ee4d7a42c7a50d38ec08eeca24f6e9af proper HTML preview; diff -r 47309113ee4d -r 38fbf13f7986 src/Tools/VSCode/extension/src/preview.ts --- a/src/Tools/VSCode/extension/src/preview.ts Mon May 29 19:34:07 2017 +0200 +++ b/src/Tools/VSCode/extension/src/preview.ts Mon May 29 19:50:46 2017 +0200 @@ -15,7 +15,16 @@ provideTextDocumentContent(uri: Uri): string | Thenable { const [name, pos] = decode_location(uri) - return "Isabelle Preview: " + JSON.stringify([name, pos]) + return ` + + + + + +

Isabelle Preview

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

+ + ` } } @@ -53,7 +62,8 @@ commands.registerTextEditorCommand("isabelle.preview", editor => { const uri = encode_location(editor.document.uri, editor.selection.active) - return workspace.openTextDocument(uri).then(doc => window.showTextDocument(doc, view_column())) + return workspace.openTextDocument(uri).then(doc => + commands.executeCommand("vscode.previewHtml", uri, view_column(), "Isabelle Preview")) }) context.subscriptions.push(provider, provider_registration, command_registration)