author | wenzelm |
Thu, 25 Jun 2009 14:19:14 +0200 | |
changeset 34616 | bc923168c880 |
parent 34615 | 5e61055bf35b |
child 34624 | 5e4f33d033ba |
permissions | -rw-r--r-- |
34407 | 1 |
/* |
2 |
* Isabelle virtual file system for jEdit. |
|
3 |
* |
|
4 |
* This filesystem passes every operation on to FileVFS. Just the read and write |
|
5 |
* operations are overwritten to convert Isabelle symbols to unicode on read and |
|
6 |
* unicode to Isabelle symbols on write. |
|
7 |
* |
|
8 |
* @author Johannes Hölzl, TU Munich |
|
9 |
*/ |
|
10 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
11 |
package isabelle.jedit |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
12 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
13 |
|
34614 | 14 |
import java.io.{InputStream, OutputStream, ByteArrayInputStream, |
15 |
ByteArrayOutputStream, InputStreamReader} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
16 |
import java.awt.Component |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
17 |
|
34614 | 18 |
import org.gjt.sp.jedit.{OperatingSystem, Buffer} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
19 |
import org.gjt.sp.jedit.io |
34614 | 20 |
import org.gjt.sp.jedit.io.{VFSFile, VFSManager} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
21 |
|
34436 | 22 |
|
34614 | 23 |
object VFS |
24 |
{ |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
25 |
val BUFFER_SIZE = 1024 |
34614 | 26 |
|
27 |
def input_converter(in: InputStream): ByteArrayInputStream = |
|
28 |
{ |
|
34615 | 29 |
val reader = new InputStreamReader(in, Isabelle_System.charset) |
34436 | 30 |
val buffer = new StringBuilder |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
31 |
val array = new Array[Char](BUFFER_SIZE) |
34614 | 32 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
33 |
var finished = false |
34436 | 34 |
while (!finished) { |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
35 |
val length = reader.read(array, 0, array.length) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
36 |
if (length == -1) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
37 |
finished = true |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
38 |
else |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
39 |
buffer.append(array, 0, length) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
40 |
} |
34363 | 41 |
|
34440 | 42 |
val str = Isabelle.symbols.decode(buffer.toString) |
34615 | 43 |
new ByteArrayInputStream(str.getBytes(Isabelle_System.charset)) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
44 |
} |
34614 | 45 |
|
46 |
class OutputConverter(out: OutputStream) extends ByteArrayOutputStream |
|
47 |
{ |
|
48 |
override def close() |
|
49 |
{ |
|
34440 | 50 |
out.write(Isabelle.symbols.encode(new String(buf, 0, count)).getBytes) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
51 |
out.close() |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
52 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
53 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
54 |
|
34614 | 55 |
class File(vfs: VFS, path: String, file: VFSFile) extends VFSFile |
56 |
{ |
|
57 |
override def getVFS = vfs |
|
58 |
override def getPath = path |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
59 |
|
34614 | 60 |
override def getColor = file.getColor |
61 |
override def getDeletePath = file.getDeletePath |
|
62 |
override def getExtendedAttribute(name: String) = file.getExtendedAttribute(name) |
|
63 |
override def getIcon(expanded: Boolean, open: Boolean) = file.getIcon(expanded, open) |
|
64 |
override def getLength = file.getLength |
|
65 |
override def getName = file.getName |
|
66 |
override def getSymlinkPath = file.getSymlinkPath |
|
67 |
override def getType = file.getType |
|
68 |
override def isBinary(session: Object) = file.isBinary(session) |
|
69 |
override def isHidden = file.isHidden |
|
70 |
override def isReadable = file.isReadable |
|
71 |
override def isWriteable = file.isWriteable |
|
72 |
override def setDeletePath(path: String) = file.setDeletePath(path) |
|
73 |
override def setHidden(hidden: Boolean) = file.setHidden(hidden) |
|
74 |
override def setLength(length: Long) = file.setLength(length) |
|
75 |
override def setName(name: String) = file.setName(name) |
|
76 |
override def setPath(path: String) = file.setPath(path) |
|
77 |
override def setReadable(readable: Boolean) = file.setReadable(readable) |
|
78 |
override def setWriteable(writeable: Boolean) = file.setWriteable(writeable) |
|
79 |
override def setSymlinkPath(symlink_path: String) = file.setSymlinkPath(symlink_path) |
|
80 |
override def setType(ty: Int) = file.setType(ty) |
|
81 |
} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
82 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
83 |
|
34614 | 84 |
class VFS extends io.VFS("isabelle", VFSManager.getFileVFS.getCapabilities) |
85 |
{ |
|
86 |
private val base = VFSManager.getFileVFS |
|
34436 | 87 |
|
34614 | 88 |
private def map_file(path: String, file: VFSFile): VFSFile = |
89 |
if (file == null) null else new VFS.File(this, path, file) |
|
90 |
||
34616 | 91 |
private def drop_prefix(path: String): String = |
92 |
if (path.startsWith(Isabelle.VFS_PREFIX)) |
|
93 |
path.substring(Isabelle.VFS_PREFIX.length) |
|
94 |
else path |
|
95 |
||
96 |
private def expand_path(path: String): String = |
|
97 |
Isabelle.VFS_PREFIX + Isabelle.system.expand_path(drop_prefix(path)) |
|
98 |
||
34614 | 99 |
private def platform_path(path: String): String = |
34616 | 100 |
Isabelle.system.platform_path(drop_prefix(path)) |
34614 | 101 |
|
34616 | 102 |
|
34614 | 103 |
override def getCapabilities = base.getCapabilities |
104 |
override def getExtendedAttributes = base.getExtendedAttributes |
|
105 |
||
106 |
override def getFileName(path: String) = base.getFileName(path) |
|
107 |
override def getParentOfPath(path: String) = super.getParentOfPath(path) |
|
108 |
||
109 |
override def constructPath(parent: String, path: String): String = |
|
110 |
if (parent.endsWith("/")) parent + path |
|
111 |
else parent + "/" + path |
|
112 |
||
113 |
override def getFileSeparator = '/' |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
114 |
|
34614 | 115 |
override def getTwoStageSaveName(path: String): String = |
116 |
{ |
|
117 |
val dir = new java.io.File(platform_path(getParentOfPath(path))) |
|
118 |
if (dir.canWrite || OperatingSystem.isWindows) |
|
119 |
super.getTwoStageSaveName(path) |
|
120 |
else null |
|
121 |
} |
|
122 |
||
123 |
override def createVFSSession(path: String, comp: Component) = base.createVFSSession(path, comp) |
|
124 |
||
34616 | 125 |
override def _canonPath(session: Object, path: String, comp: Component) = expand_path(path) |
34614 | 126 |
|
127 |
override def _listFiles(session: Object, path: String, comp: Component): Array[VFSFile] = |
|
128 |
base._listFiles(session, platform_path(path), comp).map(file => |
|
34616 | 129 |
if (file == null) null else map_file(constructPath(path, file.getName), file)) |
34614 | 130 |
|
131 |
override def _getFile(session: Object, path: String, comp: Component) = |
|
132 |
map_file(path, base._getFile(session, platform_path(path), comp)) |
|
133 |
||
134 |
override def _delete(session: Object, path: String, comp: Component) = |
|
135 |
base._delete(session, platform_path(path), comp) |
|
136 |
||
137 |
override def _rename(session: Object, from: String, to: String, comp: Component) = |
|
138 |
base._rename(session, platform_path(from), platform_path(to), comp) |
|
139 |
||
140 |
override def _mkdir(session: Object, path: String, comp: Component) = |
|
141 |
base._mkdir(session, platform_path(path), comp) |
|
142 |
||
143 |
override def _backup(session: Object, path: String, comp: Component) = |
|
144 |
base._backup(session, platform_path(path), comp) |
|
145 |
||
34436 | 146 |
override def _createInputStream(session: Object, path: String, |
147 |
ignoreErrors: Boolean, comp: Component) = |
|
34614 | 148 |
VFS.input_converter(base._createInputStream(session, platform_path(path), ignoreErrors, comp)) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
149 |
|
34614 | 150 |
override def _createOutputStream(session: Object, path: String, comp: Component) = |
151 |
new VFS.OutputConverter(base._createOutputStream(session, platform_path(path), comp)) |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
152 |
|
34436 | 153 |
override def _saveComplete(session: Object, buffer: Buffer, path: String, comp: Component) = |
34614 | 154 |
base._saveComplete(session, buffer, platform_path(path), comp) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
155 |
} |