# HG changeset patch
# User wenzelm
# Date 1496063792 -7200
# Node ID 6338355b2a88a9973418604d1ed8a1876ab2624b
# Parent  639eb3617a86fed35f64d1ecb964dcd3b7fd5a4a
basic setup for document preview;

diff -r 639eb3617a86 -r 6338355b2a88 src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Mon May 29 09:14:15 2017 +0200
+++ b/src/Tools/VSCode/extension/package.json	Mon May 29 15:16:32 2017 +0200
@@ -22,6 +22,12 @@
     ],
     "main": "./out/src/extension",
     "contributes": {
+        "commands": [
+            {
+                "command": "isabelle.preview",
+                "title": "Isabelle Document Preview"
+            }
+        ],
         "languages": [
             {
                 "id": "isabelle",
diff -r 639eb3617a86 -r 6338355b2a88 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Mon May 29 09:14:15 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Mon May 29 15:16:32 2017 +0200
@@ -5,6 +5,7 @@
 import * as fs from 'fs';
 import * as os from 'os';
 import * as decorations from './decorations';
+import * as preview from './preview';
 import * as protocol from './protocol';
 import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType }
   from 'vscode-languageclient';
@@ -106,6 +107,11 @@
     })
 
 
+    /* preview */
+
+    preview.init(context)
+
+
     /* start server */
 
     context.subscriptions.push(client.start());
diff -r 639eb3617a86 -r 6338355b2a88 src/Tools/VSCode/extension/src/preview.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/preview.ts	Mon May 29 15:16:32 2017 +0200
@@ -0,0 +1,49 @@
+'use strict';
+
+import { TextDocumentContentProvider, ExtensionContext, Uri, Position,
+  workspace, window, commands } from 'vscode'
+
+
+const uri_scheme = 'isabelle-preview';
+
+class Provider implements TextDocumentContentProvider
+{
+	constructor() { }
+
+  dispose() { }
+
+  provideTextDocumentContent(uri: Uri): string | Thenable<string>
+  {
+    const [name, pos] = decode_location(uri)
+    return "Isabelle Preview: " + JSON.stringify([name, pos])
+  }
+}
+
+export function encode_location(uri: Uri, pos: Position): Uri
+{
+  const query = JSON.stringify([uri.toString(), pos.line, pos.character])
+  return Uri.parse(uri_scheme + ":Preview?" + query)
+}
+
+export function decode_location(uri: Uri): [Uri, Position]
+{
+	let [name, line, character] = <[string, number, number]>JSON.parse(uri.query)
+	return [Uri.parse(name), new Position(line, character)]
+}
+
+export function init(context: ExtensionContext)
+{
+  const provider = new Provider()
+
+  const provider_registration =
+    workspace.registerTextDocumentContentProvider(uri_scheme, provider)
+
+ 	const command_registration =
+    commands.registerTextEditorCommand("isabelle.preview", editor =>
+    {
+      const uri = encode_location(editor.document.uri, editor.selection.active)
+      return workspace.openTextDocument(uri).then(doc => window.showTextDocument(doc, editor.viewColumn + 1))
+  	})
+
+  context.subscriptions.push(provider, provider_registration, command_registration)
+}