proper treatment of root as directory;
authorwenzelm
Sun, 28 Apr 2019 12:34:56 +0200
changeset 70203 cd2af90360ee
parent 70202 373eb0aa97e3
child 70204 230188a56a9e
proper treatment of root as directory;
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