# HG changeset patch
# User wenzelm
# Date 1548879501 -3600
# Node ID 4b0a11d499e2d6284dec4cd1d3b86eca3fe2bfea
# Parent  58fb0d7795834cccb329f389640047b1492d1367
open session ROOT file;

diff -r 58fb0d779583 -r 4b0a11d499e2 src/Tools/jEdit/src/isabelle_session.scala
--- a/src/Tools/jEdit/src/isabelle_session.scala	Wed Jan 30 16:44:29 2019 +0100
+++ b/src/Tools/jEdit/src/isabelle_session.scala	Wed Jan 30 21:18:21 2019 +0100
@@ -13,7 +13,7 @@
 import java.io.InputStream
 
 import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.io.VFSFile
+import org.gjt.sp.jedit.io.{VFS => JEdit_VFS, VFSFile}
 import org.gjt.sp.jedit.browser.VFSBrowser
 
 
@@ -29,6 +29,14 @@
 
   val vfs_prefix = "isabelle-session:"
 
+  class Session_Entry(name: String, path: String)
+    extends VFSFile(name, path, null, VFSFile.FILE, 0L, false)
+  {
+    override def getExtendedAttribute(att: String): String =
+      if (att == JEdit_VFS.EA_SIZE) null
+      else super.getExtendedAttribute(att)
+  }
+
   class VFS extends Isabelle_VFS(vfs_prefix,
     read = true, browse = true, low_latency = true, non_awt_session = true)
   {
@@ -45,7 +53,16 @@
               sessions.chapters.get(chapter) match {
                 case None => null
                 case Some(infos) =>
-                  infos.map(info => make_entry(chapter + "/" + info.name, is_dir = true)).toArray
+                  infos.map(info =>
+                  {
+                    val name = chapter + "/" + info.name
+                    val path =
+                      Position.File.unapply(info.pos) match {
+                        case Some(path) => File.platform_path(path)
+                        case None => null
+                      }
+                    new Session_Entry(name, path)
+                  }).toArray
               }
             case _ => null
           }