--- 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 =
{
--- 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
+ }
+ }
}