--- 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 */
--- 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"
--- 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
}
--- /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)
+ }
+}