# HG changeset patch
# User wenzelm
# Date 1548855315 -3600
# Node ID 1907222d974e95e7686a82188e7ea3c5a2a4affb
# Parent  2fc85ce1f557d686964dfbcfc12b7ab28718aaf8
clarified modules;

diff -r 2fc85ce1f557 -r 1907222d974e src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Wed Jan 30 13:25:33 2019 +0100
+++ b/src/Pure/Thy/export.scala	Wed Jan 30 14:35:15 2019 +0100
@@ -13,13 +13,10 @@
 
 object Export
 {
-  /* structured name */
+  /* name structure */
 
-  val sep_char: Char = '/'
-  val sep: String = sep_char.toString
-
-  def explode_name(s: String): List[String] = space_explode(sep_char, s)
-  def implode_name(elems: Iterable[String]): String = elems.mkString(sep)
+  def explode_name(s: String): List[String] = space_explode('/', s)
+  def implode_name(elems: Iterable[String]): String = elems.mkString("/")
 
 
   /* SQL data model */
diff -r 2fc85ce1f557 -r 1907222d974e src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Wed Jan 30 13:25:33 2019 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Jan 30 14:35:15 2019 +0100
@@ -36,6 +36,7 @@
   "src/isabelle.scala"
   "src/isabelle_encoding.scala"
   "src/isabelle_export.scala"
+  "src/isabelle_vfs.scala"
   "src/isabelle_options.scala"
   "src/isabelle_sidekick.scala"
   "src/jedit_bibtex.scala"
diff -r 2fc85ce1f557 -r 1907222d974e src/Tools/jEdit/src/isabelle_export.scala
--- a/src/Tools/jEdit/src/isabelle_export.scala	Wed Jan 30 13:25:33 2019 +0100
+++ b/src/Tools/jEdit/src/isabelle_export.scala	Wed Jan 30 14:35:15 2019 +0100
@@ -12,9 +12,8 @@
 import java.awt.Component
 import java.io.InputStream
 
-import org.gjt.sp.jedit.{Buffer, View}
-import org.gjt.sp.jedit.io.{VFS => JEditVFS, VFSFile, VFSManager}
-import org.gjt.sp.jedit.bufferio.BufferLoadRequest
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.io.VFSFile
 import org.gjt.sp.jedit.browser.VFSBrowser
 
 
@@ -22,45 +21,11 @@
 {
   /* virtual file-system */
 
-  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)
-  }
+  val vfs_prefix = "isabelle-export:"
 
-  def explode_url(url: String, component: Component = null): Option[List[String]] =
+  class VFS extends Isabelle_VFS(vfs_prefix,
+    read = true, browse = true, low_latency = true, non_awt_session = true)
   {
-    Library.try_unprefix(vfs_prefix, url) match {
-      case Some(path) => Some(Export.explode_name(path).filter(_.nonEmpty))
-      case None =>
-        if (component != null) vfs_error(component, url, "ioerror.badurl", url)
-        None
-    }
-  }
-
-  class VFS extends JEditVFS(vfs_name, vfs_caps)
-  {
-    override def isMarkersFileSupported: Boolean = false
-
-    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 {
@@ -73,7 +38,7 @@
               (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
+              } yield make_entry(node_name.theory, is_dir = true)).toArray
             case theory :: prefix =>
               val depth = prefix.length + 1
               val entries: List[(String, Option[Long])] =
@@ -89,8 +54,8 @@
                 }).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)
+                  case None => make_entry(path, is_dir = true)
+                  case Some(size) => make_entry(path, size = size)
                 }
               }).toArray
           }
diff -r 2fc85ce1f557 -r 1907222d974e src/Tools/jEdit/src/isabelle_vfs.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/isabelle_vfs.scala	Wed Jan 30 14:35:15 2019 +0100
@@ -0,0 +1,74 @@
+/*  Title:      Tools/jEdit/src/isabelle_vfs.scala
+    Author:     Makarius
+
+Support for virtual file-systems.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.Component
+
+import org.gjt.sp.jedit.io.{VFS, VFSManager, VFSFile}
+
+
+class Isabelle_VFS(prefix: String,
+  read: Boolean = false,
+  write: Boolean = false,
+  browse: Boolean = false,
+  delete: Boolean = false,
+  rename: Boolean = false,
+  mkdir: Boolean = false,
+  low_latency: Boolean = false,
+  case_insensitive: Boolean = false,
+  non_awt_session: Boolean = false)
+  extends VFS(Library.perhaps_unsuffix(":", prefix),
+    (if (read) VFS.READ_CAP else 0) |
+    (if (write) VFS.WRITE_CAP else 0) |
+    (if (browse) VFS.BROWSE_CAP else 0) |
+    (if (delete) VFS.DELETE_CAP else 0) |
+    (if (rename) VFS.RENAME_CAP else 0) |
+    (if (mkdir) VFS.MKDIR_CAP else 0) |
+    (if (low_latency) VFS.LOW_LATENCY_CAP else 0) |
+    (if (case_insensitive) VFS.CASE_INSENSITIVE_CAP else 0) |
+    (if (non_awt_session) VFS.NON_AWT_SESSION_CAP else 0))
+{
+  /* URL structure */
+
+  def separator: Char = '/'
+
+  def explode_name(s: String): List[String] = space_explode(separator, s)
+  def implode_name(elems: Iterable[String]): String = elems.mkString(separator.toString)
+
+  def explode_url(url: String, component: Component = null): Option[List[String]] =
+  {
+    Library.try_unprefix(prefix, url) match {
+      case Some(path) => Some(explode_name(path).filter(_.nonEmpty))
+      case None =>
+        if (component != null) VFSManager.error(component, url, "ioerror.badurl", Array(url))
+        None
+    }
+  }
+  def implode_url(elems: Iterable[String]): String = prefix + implode_name(elems)
+
+  override def constructPath(parent: String, path: String): String =
+  {
+    if (parent == "") path
+    else if (parent(parent.length - 1) == separator || parent == prefix) parent + path
+    else parent + separator + path
+  }
+
+
+  /* directory content */
+
+  override def isMarkersFileSupported: Boolean = false
+
+  def make_entry(path: String, is_dir: Boolean = false, size: Long = 0L): VFSFile =
+  {
+    val entry = explode_name(path).lastOption getOrElse ""
+    val url = prefix + path
+    new VFSFile(entry, url, url, if (is_dir) VFSFile.DIRECTORY else VFSFile.FILE, size, false)
+  }
+}