69756
|
1 |
/* Title: Tools/jEdit/src/isabelle_vfs.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Support for virtual file-systems.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle.jedit
|
|
8 |
|
|
9 |
|
|
10 |
import isabelle._
|
|
11 |
|
|
12 |
import java.awt.Component
|
|
13 |
|
|
14 |
import org.gjt.sp.jedit.io.{VFS, VFSManager, VFSFile}
|
|
15 |
|
|
16 |
|
|
17 |
class 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 separator: Char = '/'
|
|
41 |
|
|
42 |
def explode_name(s: String): List[String] = space_explode(separator, s)
|
|
43 |
def implode_name(elems: Iterable[String]): String = elems.mkString(separator.toString)
|
|
44 |
|
|
45 |
def explode_url(url: String, component: Component = null): Option[List[String]] =
|
|
46 |
{
|
|
47 |
Library.try_unprefix(prefix, url) match {
|
|
48 |
case Some(path) => Some(explode_name(path).filter(_.nonEmpty))
|
|
49 |
case None =>
|
|
50 |
if (component != null) VFSManager.error(component, url, "ioerror.badurl", Array(url))
|
|
51 |
None
|
|
52 |
}
|
|
53 |
}
|
|
54 |
def implode_url(elems: Iterable[String]): String = prefix + implode_name(elems)
|
|
55 |
|
|
56 |
override def constructPath(parent: String, path: String): String =
|
|
57 |
{
|
|
58 |
if (parent == "") path
|
|
59 |
else if (parent(parent.length - 1) == separator || parent == prefix) parent + path
|
|
60 |
else parent + separator + path
|
|
61 |
}
|
|
62 |
|
|
63 |
|
|
64 |
/* directory content */
|
|
65 |
|
|
66 |
override def isMarkersFileSupported: Boolean = false
|
|
67 |
|
|
68 |
def make_entry(path: String, is_dir: Boolean = false, size: Long = 0L): VFSFile =
|
|
69 |
{
|
|
70 |
val entry = explode_name(path).lastOption getOrElse ""
|
|
71 |
val url = prefix + path
|
|
72 |
new VFSFile(entry, url, url, if (is_dir) VFSFile.DIRECTORY else VFSFile.FILE, size, false)
|
|
73 |
}
|
|
74 |
}
|