diff -r dd1e0e1570d2 -r f3b564a13236 src/Tools/jEdit/src/isabelle_export.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/isabelle_export.scala	Fri Jan 11 22:55:02 2019 +0100
@@ -0,0 +1,117 @@
+/*  Title:      Tools/jEdit/src/isabelle_export.scala
+    Author:     Makarius
+
+Access Isabelle theory exports via virtual file-system.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.Component
+import java.io.InputStream
+
+import org.gjt.sp.jedit.io.{VFS => JEditVFS, VFSFile, VFSManager}
+
+
+object Isabelle_Export
+{
+  val vfs_name = "isabelle-export"
+  val vfs_caps =
+    JEditVFS.READ_CAP |
+    JEditVFS.BROWSE_CAP |
+    JEditVFS.LOW_LATENCY_CAP |
+    JEditVFS.NON_AWT_SESSION_CAP
+
+  val vfs_prefix = vfs_name + ":"
+
+  def vfs_error(component: Component, path: String, prop: String, args: AnyRef*): Unit =
+    VFSManager.error(component, path, prop, args.toArray)
+
+  def vfs_file(path: String, is_dir: Boolean = false, size: Long = 0L): VFSFile =
+  {
+    val name = Export.explode_name(path).lastOption getOrElse ""
+    val url = vfs_prefix + path
+    new VFSFile(name, url, url, if (is_dir) VFSFile.DIRECTORY else VFSFile.FILE, size, false)
+  }
+
+  def explode_url(url: String, component: Component = null): Option[List[String]] =
+  {
+    def bad: None.type =
+    {
+      if (component != null) vfs_error(component, url, "ioerror.badurl", url)
+      None
+    }
+    Library.try_unprefix(vfs_prefix, url) match {
+      case Some(path) =>
+        val elems = Export.explode_name(path)
+        if (elems.exists(_.isEmpty)) bad else Some(elems)
+      case None => bad
+    }
+  }
+
+  class VFS extends JEditVFS(vfs_name, vfs_caps)
+  {
+    override def constructPath(parent: String, path: String): String =
+    {
+      if (parent == vfs_prefix || parent.endsWith(Export.sep)) parent + path
+      else parent + Export.sep + path
+    }
+
+    override def _listFiles(session: AnyRef, url: String, component: Component): Array[VFSFile] =
+    {
+      explode_url(url, component = component) match {
+        case None => null
+        case Some(elems) =>
+          val snapshot = PIDE.snapshot()
+          val version = snapshot.version
+          elems match {
+            case Nil =>
+              (for {
+                (node_name, _) <- version.nodes.iterator
+                if !snapshot.state.node_exports(version, node_name).is_empty
+              } yield vfs_file(node_name.theory, is_dir = true)).toArray
+            case theory :: prefix =>
+              val depth = prefix.length + 1
+              val entries: List[(String, Option[Long])] =
+                (for {
+                  (node_name, _) <- version.nodes.iterator if node_name.theory == theory
+                  exports = snapshot.state.node_exports(version, node_name)
+                  (_, entry) <- exports.iterator if entry.name_extends(prefix)
+                } yield {
+                  val is_dir = entry.name_elems.length > depth
+                  val path = Export.implode_name(theory :: entry.name_elems.take(depth))
+                  val file_size = if (is_dir) None else Some(entry.uncompressed().length.toLong)
+                  (path, file_size)
+                }).toSet.toList
+              (for ((path, file_size) <- entries.iterator) yield {
+                file_size match {
+                  case None => vfs_file(path, is_dir = true)
+                  case Some(size) => vfs_file(path, size = size)
+                }
+              }).toArray
+          }
+      }
+    }
+
+    override def _createInputStream(
+      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()
+        case Some(theory :: name_elems) =>
+          val snapshot = PIDE.snapshot()
+          val version = snapshot.version
+          val bytes =
+            (for {
+              (node_name, _) <- version.nodes.iterator
+              if node_name.theory == theory
+              (_, entry) <- snapshot.state.node_exports(version, node_name).iterator
+              if entry.name_elems == name_elems
+            } yield entry.uncompressed()).find(_ => true).getOrElse(Bytes.empty)
+          bytes.stream()
+      }
+    }
+  }
+}