proper HTML preview;
authorwenzelm
Mon, 29 May 2017 19:50:46 +0200
changeset 65960 38fbf13f7986
parent 65959 47309113ee4d
child 65961 7f87310d6c09
proper HTML preview;
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<string>
   {
     const [name, pos] = decode_location(uri)
-    return "Isabelle Preview: " + JSON.stringify([name, pos])
+    return `
+      <html>
+      <head>
+        <meta http-equiv="Content-type" content="text/html; charset=UTF-8">
+      </head>
+      <body>
+        <h1>Isabelle Preview</h1>
+        <p>${JSON.stringify([name, pos])}</p>
+      </body>
+      </html>`
   }
 }
 
@@ -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)