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