removed pointless default: vscode.previewHtml happens only after prover response;
authorwenzelm
Mon, 12 Jun 2017 11:41:54 +0200
changeset 66068 f8899f6071ac
parent 66067 cdbcb417db67
child 66069 0a34bfc15e2c
removed pointless default: vscode.previewHtml happens only after prover response;
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<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()) || ""
   }
 }