# HG changeset patch # User wenzelm # Date 1497260514 -7200 # Node ID f8899f6071ac9e6aef7396efabc121862df55cd7 # Parent cdbcb417db67051d0d3860f0588304156727b69c removed pointless default: vscode.previewHtml happens only after prover response; diff -r cdbcb417db67 -r f8899f6071ac src/Tools/VSCode/extension/src/preview.ts --- a/src/Tools/VSCode/extension/src/preview.ts Mon Jun 12 11:32:23 2017 +0200 +++ b/src/Tools/VSCode/extension/src/preview.ts Mon Jun 12 11:41:54 2017 +0200 @@ -35,16 +35,6 @@ const preview_content = new Map() -const default_preview_content = - ` - - - - -

Isabelle Preview

- - ` - class Content_Provider implements TextDocumentContentProvider { dispose() { } @@ -55,7 +45,7 @@ provideTextDocumentContent(preview_uri: Uri): string { - return preview_content.get(preview_uri.toString()) || default_preview_content + return preview_content.get(preview_uri.toString()) || "" } }