# HG changeset patch
# User wenzelm
# Date 1548862326 -3600
# Node ID a899ca03d74ca60cfe14f80ec6d7527ce29da76e
# Parent  d0a6e1160be354f15a216d175960606ea13290e2
clarified modules;

diff -r d0a6e1160be3 -r a899ca03d74c src/Tools/jEdit/src/isabelle_export.scala
--- a/src/Tools/jEdit/src/isabelle_export.scala	Wed Jan 30 16:12:01 2019 +0100
+++ b/src/Tools/jEdit/src/isabelle_export.scala	Wed Jan 30 16:32:06 2019 +0100
@@ -62,17 +62,6 @@
       }
     }
 
-    override def _getFile(vfs_session: AnyRef, url: String, component: Component): VFSFile =
-    {
-      val parent = getParentOfPath(url)
-      if (parent == vfs_prefix) null
-      else {
-        val files = _listFiles(vfs_session, parent, component)
-        if (files == null) null
-        else files.find(_.getPath == url) getOrElse null
-      }
-    }
-
     override def _createInputStream(
       vfs_session: AnyRef, url: String, ignore_errors: Boolean, component: Component): InputStream =
     {
diff -r d0a6e1160be3 -r a899ca03d74c src/Tools/jEdit/src/isabelle_vfs.scala
--- a/src/Tools/jEdit/src/isabelle_vfs.scala	Wed Jan 30 16:12:01 2019 +0100
+++ b/src/Tools/jEdit/src/isabelle_vfs.scala	Wed Jan 30 16:32:06 2019 +0100
@@ -69,4 +69,15 @@
     val url = prefix + path
     new VFSFile(entry, url, url, if (is_dir) VFSFile.DIRECTORY else VFSFile.FILE, size, false)
   }
+
+  override def _getFile(vfs_session: AnyRef, url: String, component: Component): VFSFile =
+  {
+    val parent = getParentOfPath(url)
+    if (parent == prefix) null
+    else {
+      val files = _listFiles(vfs_session, parent, component)
+      if (files == null) null
+      else files.find(_.getPath == url) getOrElse null
+    }
+  }
 }