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