# HG changeset patch
# User wenzelm
# Date 1498735688 -7200
# Node ID eec1c99e1bdcf4ad31711ad4908670b28baf211f
# Parent  9380ec9babfb5b899102ef321ec6a6c09312e833
tuned signature;

diff -r 9380ec9babfb -r eec1c99e1bdc src/Tools/VSCode/extension/src/library.ts
--- a/src/Tools/VSCode/extension/src/library.ts	Thu Jun 29 11:58:00 2017 +0200
+++ b/src/Tools/VSCode/extension/src/library.ts	Thu Jun 29 13:28:08 2017 +0200
@@ -1,7 +1,7 @@
 'use strict';
 
 import * as os from 'os';
-import { TextEditor, Uri, ViewColumn, workspace } from 'vscode'
+import { TextEditor, Uri, ViewColumn, workspace, window } from 'vscode'
 
 
 /* regular expressions */
@@ -20,13 +20,23 @@
 }
 
 
-/* file URIs */
+/* files */
 
 export function is_file(uri: Uri): boolean
 {
   return uri.scheme === "file"
 }
 
+export function find_file_editor(uri: Uri): TextEditor | undefined
+{
+  if (is_file(uri)) {
+    return window.visibleTextEditors.find(editor =>
+      is_file(editor.document.uri) && editor.document.uri.fsPath === uri.fsPath)
+  }
+  else return undefined
+}
+
+
 
 /* Isabelle configuration */
 
diff -r 9380ec9babfb -r eec1c99e1bdc src/Tools/VSCode/extension/src/preview_panel.ts
--- a/src/Tools/VSCode/extension/src/preview_panel.ts	Thu Jun 29 11:58:00 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview_panel.ts	Thu Jun 29 13:28:08 2017 +0200
@@ -85,10 +85,7 @@
 {
   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)
+    const editor = library.find_file_editor(document_uri)
     if (editor) window.showTextDocument(editor.document, editor.viewColumn)
     else workspace.openTextDocument(document_uri).then(window.showTextDocument)
   }