removed pointless default: vscode.previewHtml happens only after prover response;
--- 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<string, string>()
-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>`
-
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()) || ""
}
}