# HG changeset patch
# User wenzelm
# Date 1547324495 -3600
# Node ID fc2b565fa37725b85dc25da9b6272b32ff816675
# Parent  af09cc4792dc34d778883d86019982585882f19a
proper _getFile method -- required to open files from browser;

diff -r af09cc4792dc -r fc2b565fa377 src/Tools/jEdit/src/isabelle_export.scala
--- a/src/Tools/jEdit/src/isabelle_export.scala	Sat Jan 12 20:14:05 2019 +0100
+++ b/src/Tools/jEdit/src/isabelle_export.scala	Sat Jan 12 21:21:35 2019 +0100
@@ -12,7 +12,9 @@
 import java.awt.Component
 import java.io.InputStream
 
+import org.gjt.sp.jedit.{Buffer, View}
 import org.gjt.sp.jedit.io.{VFS => JEditVFS, VFSFile, VFSManager}
+import org.gjt.sp.jedit.bufferio.BufferLoadRequest
 
 
 object Isabelle_Export
@@ -90,6 +92,17 @@
       }
     }
 
+    override def _getFile(session: AnyRef, url: String, component: Component): VFSFile =
+    {
+      val parent = getParentOfPath(url)
+      if (parent == vfs_prefix) null
+      else {
+        val files = _listFiles(session, parent, component)
+        if (files == null) null
+        else files.find(_.getPath == url) getOrElse null
+      }
+    }
+
     override def _createInputStream(
       session: AnyRef, url: String, ignore_errors: Boolean, component: Component): InputStream =
     {