# HG changeset patch
# User wenzelm
# Date 1498575040 -7200
# Node ID 5763d9a2f47d78a92d9613da16c1e37617a7ed19
# Parent  fed3690d3b4dee93a3b48651c17d0387a395b47f
added missing files (cf. 5aa9cb83e70e);

diff -r fed3690d3b4d -r 5763d9a2f47d src/Tools/VSCode/extension/src/preview_panel.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/preview_panel.ts	Tue Jun 27 16:50:40 2017 +0200
@@ -0,0 +1,96 @@
+'use strict';
+
+import * as timers from 'timers'
+import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider,
+  ExtensionContext, Event, EventEmitter, Uri, Position, workspace,
+  window, commands } from 'vscode'
+import { LanguageClient } from 'vscode-languageclient';
+import * as library from './library'
+import * as protocol from './protocol'
+import { Content_Provider } from './content_provider'
+
+
+/* HTML content */
+
+const content_provider = new Content_Provider("isabelle-preview")
+
+function encode_preview(document_uri: Uri | undefined): Uri | undefined
+{
+  if (document_uri && library.is_file(document_uri)) {
+    return content_provider.uri_template.with({ query: document_uri.fsPath })
+  }
+  else undefined
+}
+
+function decode_preview(preview_uri: Uri | undefined): Uri | undefined
+{
+  if (preview_uri && preview_uri.scheme === content_provider.uri_scheme) {
+    return Uri.file(preview_uri.query)
+  }
+  else undefined
+}
+
+
+/* setup */
+
+let language_client: LanguageClient
+
+export function setup(context: ExtensionContext, client: LanguageClient)
+{
+  context.subscriptions.push(content_provider.register())
+
+  language_client = client
+  language_client.onNotification(protocol.preview_response_type, params =>
+    {
+      const preview_uri = encode_preview(Uri.parse(params.uri))
+      if (preview_uri) {
+        content_provider.set_content(preview_uri, params.content)
+        content_provider.update(preview_uri)
+
+        const existing_document =
+          workspace.textDocuments.find(document =>
+            document.uri.scheme === preview_uri.scheme &&
+            document.uri.query === preview_uri.query)
+        if (!existing_document && params.column != 0) {
+          commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label)
+        }
+      }
+    })
+}
+
+
+/* commands */
+
+export function request(uri?: Uri, split: boolean = false)
+{
+  const document_uri = uri || window.activeTextEditor.document.uri
+  const preview_uri = encode_preview(document_uri)
+  if (preview_uri && language_client) {
+    language_client.sendNotification(protocol.preview_request_type,
+      { uri: document_uri.toString(),
+        column: library.adjacent_editor_column(window.activeTextEditor, split) })
+  }
+}
+
+export function update(preview_uri: Uri)
+{
+  const document_uri = decode_preview(preview_uri)
+  if (document_uri && language_client) {
+    language_client.sendNotification(protocol.preview_request_type,
+      { uri: document_uri.toString(), column: 0 })
+  }
+}
+
+export function source(preview_uri: Uri)
+{
+  const document_uri = decode_preview(preview_uri)
+  if (document_uri) {
+    const editor =
+      window.visibleTextEditors.find(editor =>
+        library.is_file(editor.document.uri) &&
+        editor.document.uri.fsPath === document_uri.fsPath)
+    if (editor) window.showTextDocument(editor.document, editor.viewColumn)
+    else workspace.openTextDocument(document_uri).then(window.showTextDocument)
+  }
+  else commands.executeCommand("workbench.action.navigateBack")
+}
diff -r fed3690d3b4d -r 5763d9a2f47d src/Tools/VSCode/extension/src/state_panel.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/state_panel.ts	Tue Jun 27 16:50:40 2017 +0200
@@ -0,0 +1,78 @@
+'use strict';
+
+import * as library from './library'
+import * as protocol from './protocol'
+import { Content_Provider } from './content_provider'
+import { LanguageClient } from 'vscode-languageclient';
+import { Uri, ExtensionContext, workspace, commands, window } from 'vscode'
+
+
+/* HTML content */
+
+const content_provider = new Content_Provider("isabelle-state")
+
+function encode_state(id: number | undefined): Uri | undefined
+{
+  return id ? content_provider.uri_template.with({ fragment: id.toString() }) : undefined
+}
+
+function decode_state(uri: Uri | undefined): number | undefined
+{
+  if (uri && uri.scheme === content_provider.uri_scheme) {
+    const id = parseInt(uri.fragment)
+    return id ? id : undefined
+  }
+  else undefined
+}
+
+
+/* setup */
+
+let language_client: LanguageClient
+
+export function setup(context: ExtensionContext, client: LanguageClient)
+{
+  context.subscriptions.push(content_provider.register())
+
+  language_client = client
+  language_client.onNotification(protocol.state_output_type, params =>
+    {
+      const uri = encode_state(params.id)
+      if (uri) {
+        content_provider.set_content(uri, params.content)
+        content_provider.update(uri)
+
+        const existing_document =
+          workspace.textDocuments.find(document =>
+            document.uri.scheme === uri.scheme &&
+            document.uri.fragment === uri.fragment)
+        if (!existing_document) {
+          const column = library.adjacent_editor_column(window.activeTextEditor, true)
+          commands.executeCommand("vscode.previewHtml", uri, column, "State")
+        }
+      }
+    })
+}
+
+
+/* commands */
+
+export function init(uri: Uri)
+{
+  if (language_client) language_client.sendNotification(protocol.state_init_type)
+}
+
+export function exit(id: number)
+{
+  if (language_client) language_client.sendNotification(protocol.state_exit_type, { id: id })
+}
+
+export function locate(id: number)
+{
+  if (language_client) language_client.sendNotification(protocol.state_locate_type, { id: id })
+}
+
+export function update(id: number)
+{
+  if (language_client) language_client.sendNotification(protocol.state_update_type, { id: id })
+}