# HG changeset patch # User wenzelm # Date 1556447696 -7200 # Node ID cd2af90360eeddc1c5812dfff0c63983c95079ad # Parent 373eb0aa97e302dc86687edb6a5fed436f3aaccc proper treatment of root as directory; diff -r 373eb0aa97e3 -r cd2af90360ee src/Tools/jEdit/src/isabelle_vfs.scala --- a/src/Tools/jEdit/src/isabelle_vfs.scala Sat Apr 27 21:56:59 2019 +0100 +++ b/src/Tools/jEdit/src/isabelle_vfs.scala Sun Apr 28 12:34:56 2019 +0200 @@ -73,7 +73,7 @@ override def _getFile(vfs_session: AnyRef, url: String, component: Component): VFSFile = { val parent = getParentOfPath(url) - if (parent == prefix) null + if (parent == prefix) new VFSFile(prefix, prefix, prefix, VFSFile.DIRECTORY, 0L, false) else { val files = _listFiles(vfs_session, parent, component) if (files == null) null