src/Tools/VSCode/extension/src/library.ts

--- a/src/Tools/VSCode/extension/src/library.ts	Thu Jun 29 13:28:08 2017 +0200
+++ b/src/Tools/VSCode/extension/src/library.ts	Thu Jun 29 14:39:24 2017 +0200
@@ -29,15 +29,17 @@
 
 export function find_file_editor(uri: Uri): TextEditor | undefined
 {
+  function check(editor: TextEditor): boolean
+  { return editor && is_file(editor.document.uri) && editor.document.uri.fsPath === uri.fsPath }
+
   if (is_file(uri)) {
-    return window.visibleTextEditors.find(editor =>
-      is_file(editor.document.uri) && editor.document.uri.fsPath === uri.fsPath)
+    if (check(window.activeTextEditor)) return window.activeTextEditor
+    else return window.visibleTextEditors.find(check)
   }
   else return undefined
 }
 
 
-
 /* Isabelle configuration */
 
 export function get_configuration<T>(name: string): T