# HG changeset patch # User wenzelm # Date 1548861121 -3600 # Node ID d0a6e1160be354f15a216d175960606ea13290e2 # Parent 092c6a4bcc2613b7ae34dba789e0e456d08f5172 tuned; diff -r 092c6a4bcc26 -r d0a6e1160be3 src/Tools/jEdit/src/isabelle_export.scala --- a/src/Tools/jEdit/src/isabelle_export.scala Wed Jan 30 16:07:06 2019 +0100 +++ b/src/Tools/jEdit/src/isabelle_export.scala Wed Jan 30 16:12:01 2019 +0100 @@ -26,7 +26,7 @@ class VFS extends Isabelle_VFS(vfs_prefix, read = true, browse = true, low_latency = true, non_awt_session = true) { - override def _listFiles(session: AnyRef, url: String, component: Component): Array[VFSFile] = + override def _listFiles(vfs_session: AnyRef, url: String, component: Component): Array[VFSFile] = { explode_url(url, component = component) match { case None => null @@ -62,19 +62,19 @@ } } - override def _getFile(session: AnyRef, url: String, component: Component): VFSFile = + override def _getFile(vfs_session: AnyRef, url: String, component: Component): VFSFile = { val parent = getParentOfPath(url) if (parent == vfs_prefix) null else { - val files = _listFiles(session, parent, component) + val files = _listFiles(vfs_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 = + vfs_session: AnyRef, url: String, ignore_errors: Boolean, component: Component): InputStream = { explode_url(url, component = if (ignore_errors) null else component) match { case None | Some(Nil) => Bytes.empty.stream()