tuned signature;

--- 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 */
 

--- 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)
   }