1/*  Title:      Tools/jEdit/src/isabelle_vfs.scala
2    Author:     Makarius
3
4Support for virtual file-systems.
5*/
6
7package isabelle.jedit
8
9
10import isabelle._
11
12import java.awt.Component
13
14import org.gjt.sp.jedit.io.{VFS, VFSManager, VFSFile}
15
16
17class Isabelle_VFS(prefix: String,
18  read: Boolean = false,
19  write: Boolean = false,
20  browse: Boolean = false,
21  delete: Boolean = false,
22  rename: Boolean = false,
23  mkdir: Boolean = false,
24  low_latency: Boolean = false,
25  case_insensitive: Boolean = false,
26  non_awt_session: Boolean = false)
27  extends VFS(Library.perhaps_unsuffix(":", prefix),
28    (if (read) VFS.READ_CAP else 0) |
29    (if (write) VFS.WRITE_CAP else 0) |
30    (if (browse) VFS.BROWSE_CAP else 0) |
31    (if (delete) VFS.DELETE_CAP else 0) |
32    (if (rename) VFS.RENAME_CAP else 0) |
33    (if (mkdir) VFS.MKDIR_CAP else 0) |
34    (if (low_latency) VFS.LOW_LATENCY_CAP else 0) |
35    (if (case_insensitive) VFS.CASE_INSENSITIVE_CAP else 0) |
36    (if (non_awt_session) VFS.NON_AWT_SESSION_CAP else 0))
37{
38  /* URL structure */
39
40  def explode_name(s: String): List[String] = space_explode(getFileSeparator, s)
41  def implode_name(elems: Iterable[String]): String = elems.mkString(getFileSeparator.toString)
42
43  def explode_url(url: String, component: Component = null): Option[List[String]] =
44  {
45    Library.try_unprefix(prefix, url) match {
46      case Some(path) => Some(explode_name(path).filter(_.nonEmpty))
47      case None =>
48        if (component != null) VFSManager.error(component, url, "ioerror.badurl", Array(url))
49        None
50    }
51  }
52  def implode_url(elems: Iterable[String]): String = prefix + implode_name(elems)
53
54  override def constructPath(parent: String, path: String): String =
55  {
56    if (parent == "") path
57    else if (parent(parent.length - 1) == getFileSeparator || parent == prefix) parent + path
58    else parent + getFileSeparator + path
59  }
60
61
62  /* directory content */
63
64  override def isMarkersFileSupported: Boolean = false
65
66  def make_entry(path: String, is_dir: Boolean = false, size: Long = 0L): VFSFile =
67  {
68    val entry = explode_name(path).lastOption getOrElse ""
69    val url = prefix + path
70    new VFSFile(entry, url, url, if (is_dir) VFSFile.DIRECTORY else VFSFile.FILE, size, false)
71  }
72
73  override def _getFile(vfs_session: AnyRef, url: String, component: Component): VFSFile =
74  {
75    val parent = getParentOfPath(url)
76    if (parent == prefix) new VFSFile(prefix, prefix, prefix, VFSFile.DIRECTORY, 0L, false)
77    else {
78      val files = _listFiles(vfs_session, parent, component)
79      if (files == null) null
80      else files.find(_.getPath == url) getOrElse null
81    }
82  }
83}
84