misc tuning and reorganization;
authorwenzelm
Thu, 25 Jun 2009 00:36:20 +0200
changeset 34614 25b178e4faaf
parent 34613 71fb6ab6ec57
child 34615 5e61055bf35b
misc tuning and reorganization; Isabelle system path expansion;
src/Tools/jEdit/src/jedit/VFS.scala
--- a/src/Tools/jEdit/src/jedit/VFS.scala	Tue Jun 23 21:14:54 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/VFS.scala	Thu Jun 25 00:36:20 2009 +0200
@@ -11,24 +11,25 @@
 package isabelle.jedit
 
 
-import java.io.{InputStream, OutputStream, ByteArrayInputStream, ByteArrayOutputStream, InputStreamReader}
+import java.io.{InputStream, OutputStream, ByteArrayInputStream,
+  ByteArrayOutputStream, InputStreamReader}
 import java.awt.Component
 
-import org.gjt.sp.jedit.Buffer
-import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.{OperatingSystem, Buffer}
 import org.gjt.sp.jedit.io
-import org.gjt.sp.jedit.io.VFSFile
-import org.gjt.sp.jedit.io.VFSManager
+import org.gjt.sp.jedit.io.{VFSFile, VFSManager}
 
 
-object VFS {  
+object VFS
+{
   val BUFFER_SIZE = 1024
-  
-  def input_converter(in: InputStream) = {
+
+  def input_converter(in: InputStream): ByteArrayInputStream =
+  {
     val reader = new InputStreamReader(in, IsabelleSystem.charset)
     val buffer = new StringBuilder
     val array = new Array[Char](BUFFER_SIZE)
-    
+
     var finished = false
     while (!finished) {
       val length = reader.read(array, 0, array.length)
@@ -41,151 +42,108 @@
     val str = Isabelle.symbols.decode(buffer.toString)
     new ByteArrayInputStream(str.getBytes(IsabelleSystem.charset))
   }
-  
-  class OutputConverter(out: OutputStream) extends ByteArrayOutputStream {
-    override def close() {
+
+  class OutputConverter(out: OutputStream) extends ByteArrayOutputStream
+  {
+    override def close()
+    {
       out.write(Isabelle.symbols.encode(new String(buf, 0, count)).getBytes)
       out.close()
     }
   }
-  
-  def map_file(vfs: VFS, base: VFSFile) =
-    if (base == null) null else new File(vfs, base)
-  
-  class File(vfs: VFS, base: VFSFile) extends VFSFile {
-    // FIXME redundant overriding (!??)
-    
-    override def getColor() = 
-      base.getColor()
-    
-    override def getDeletePath() = 
-      base.getDeletePath()
-    
-    override def getExtendedAttribute(name: String) =
-      base.getExtendedAttribute(name)
 
-    override def getIcon(expanded: Boolean, openBuffer: Boolean) = 
-      base.getIcon(expanded, openBuffer)
-
-    override def getLength() = 
-      base.getLength()  
-
-    override def getName() =
-      base.getName()
-
-    override def getPath() =
-      Isabelle.VFS_PREFIX + base.getPath()
-
-    override def getSymlinkPath() =
-      base.getSymlinkPath()
-
-    override def getType() =
-      base.getType()
-
-    override def getVFS() =
-      vfs
+  class File(vfs: VFS, path: String, file: VFSFile) extends VFSFile
+  {
+    override def getVFS = vfs
+    override def getPath = path
 
-    override def isBinary(session: Object) =
-      base.isBinary(session)
-
-    override def isHidden() =
-      base.isHidden()
-
-    override def isReadable() =
-      base.isReadable()
-
-    override def isWriteable() =
-      base.isWriteable()
-
-    override def setDeletePath(path: String) =
-      base.setDeletePath(path)
-    
-    override def setHidden(hidden: Boolean) =
-      base.setHidden(hidden)
-      
-    override def setLength(length: Long) =
-      base.setLength(length)
-      
-    override def setName(name: String) =
-      base.setName(name)
-      
-    override def setPath(path: String) =
-      base.setPath(path)
-      
-    override def setReadable(readable: Boolean) =
-      base.setReadable(readable)
-      
-    override def setWriteable(writeable: Boolean) =
-      base.setWriteable(writeable)
-      
-    override def setSymlinkPath(symlinkPath: String) =
-      base.setSymlinkPath(symlinkPath)
-      
-    override def setType(fType: Int) =
-      base.setType(fType)
-  }  
+    override def getColor = file.getColor
+    override def getDeletePath = file.getDeletePath
+    override def getExtendedAttribute(name: String) = file.getExtendedAttribute(name)
+    override def getIcon(expanded: Boolean, open: Boolean) = file.getIcon(expanded, open)
+    override def getLength = file.getLength
+    override def getName = file.getName
+    override def getSymlinkPath = file.getSymlinkPath
+    override def getType = file.getType
+    override def isBinary(session: Object) = file.isBinary(session)
+    override def isHidden = file.isHidden
+    override def isReadable = file.isReadable
+    override def isWriteable = file.isWriteable
+    override def setDeletePath(path: String) = file.setDeletePath(path)
+    override def setHidden(hidden: Boolean) = file.setHidden(hidden)
+    override def setLength(length: Long) = file.setLength(length)
+    override def setName(name: String) = file.setName(name)
+    override def setPath(path: String) = file.setPath(path)
+    override def setReadable(readable: Boolean) = file.setReadable(readable)
+    override def setWriteable(writeable: Boolean) = file.setWriteable(writeable)
+    override def setSymlinkPath(symlink_path: String) = file.setSymlinkPath(symlink_path)
+    override def setType(ty: Int) = file.setType(ty)
+  }
 }
 
+class VFS extends io.VFS("isabelle", VFSManager.getFileVFS.getCapabilities)
+{
+  private val base = VFSManager.getFileVFS
 
-class VFS extends io.VFS("isabelle", VFSManager.getVFSForProtocol("file").getCapabilities) {
-  private var baseVFS = VFSManager.getVFSForProtocol("file")
+  private def map_file(path: String, file: VFSFile): VFSFile =
+    if (file == null) null else new VFS.File(this, path, file)
+
+  private def platform_path(path: String): String =
+    Isabelle.system.platform_path(
+      if (path.startsWith(Isabelle.VFS_PREFIX))
+        path.substring(Isabelle.VFS_PREFIX.length)
+      else path)
+
+  override def getCapabilities = base.getCapabilities
+  override def getExtendedAttributes = base.getExtendedAttributes
+
+  override def getFileName(path: String) = base.getFileName(path)
+  override def getParentOfPath(path: String) = super.getParentOfPath(path)
+
+  override def constructPath(parent: String, path: String): String =
+    if (parent.endsWith("/")) parent + path
+    else parent + "/" + path
+
+  override def getFileSeparator = '/'
 
-  private def cutPath(path: String) = 
-    if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length)
-    else path
-  
-  override def createVFSSession(path: String, comp: Component) = 
-    baseVFS.createVFSSession(cutPath(path), comp)
-  
-  override def getCapabilities() = 
-    baseVFS.getCapabilities()
-  
-  override def getExtendedAttributes() = 
-    baseVFS.getExtendedAttributes()
-  
-  override def getParentOfPath(path: String) = 
-    Isabelle.VFS_PREFIX + baseVFS.getParentOfPath(cutPath(path))
-  
-  override def constructPath(parent: String, path: String) = 
-    Isabelle.VFS_PREFIX + baseVFS.constructPath(cutPath(parent), path)
-  
-  override def getFileName(path: String) = 
-    baseVFS.getFileName(path)
-  
-  override def getFileSeparator() = 
-    baseVFS.getFileSeparator()
-  
-  override def getTwoStageSaveName(path: String) = 
-    Isabelle.VFS_PREFIX + baseVFS.getTwoStageSaveName(cutPath(path))
-  
-  override def _canonPath(session: Object, path: String, comp: Component) =
-    Isabelle.VFS_PREFIX + baseVFS._canonPath(session, cutPath(path), comp)
-  
+  override def getTwoStageSaveName(path: String): String =
+  {
+    val dir = new java.io.File(platform_path(getParentOfPath(path)))
+    if (dir.canWrite || OperatingSystem.isWindows)
+      super.getTwoStageSaveName(path)
+    else null
+  }
+
+  override def createVFSSession(path: String, comp: Component) = base.createVFSSession(path, comp)
+
+  override def _canonPath(session: Object, path: String, comp: Component) = path  // FIXME expand?
+
+  override def _listFiles(session: Object, path: String, comp: Component): Array[VFSFile] =
+    base._listFiles(session, platform_path(path), comp).map(file =>
+      map_file(constructPath(path, file.getName), file))
+
+  override def _getFile(session: Object, path: String, comp: Component) =
+    map_file(path, base._getFile(session, platform_path(path), comp))
+
+  override def _delete(session: Object, path: String, comp: Component) =
+    base._delete(session, platform_path(path), comp)
+
+  override def _rename(session: Object, from: String, to: String, comp: Component) =
+    base._rename(session, platform_path(from), platform_path(to), comp)
+
+  override def _mkdir(session: Object, path: String, comp: Component) =
+    base._mkdir(session, platform_path(path), comp)
+
+  override def _backup(session: Object, path: String, comp: Component) =
+    base._backup(session, platform_path(path), comp)
+
   override def _createInputStream(session: Object, path: String,
       ignoreErrors: Boolean, comp: Component) =
-    VFS.input_converter(baseVFS._createInputStream(session, cutPath(path), ignoreErrors, comp))
-  
-  override def _createOutputStream(session: Object, path: String, comp: Component) =
-    new VFS.OutputConverter(baseVFS._createOutputStream(session, cutPath(path), comp))
-  
-  override def _delete(session: Object, path: String, comp: Component) =
-    baseVFS._delete(session, cutPath(path), comp)
-  
-  override def _getFile(session: Object, path: String, comp: Component) =
-    VFS.map_file(this, baseVFS._getFile(session, cutPath(path), comp))
+    VFS.input_converter(base._createInputStream(session, platform_path(path), ignoreErrors, comp))
 
-  override def _listFiles(session: Object, path: String, comp:  Component): Array[VFSFile] =
-    (baseVFS._listFiles(session, cutPath(path), comp).map(file => VFS.map_file(this, file)))
-
-  override def _mkdir(session: Object, path: String, comp: Component) =
-    baseVFS._mkdir(session, cutPath(path), comp)
-
-  override def _rename(session: Object, from: String, to: String, comp: Component) =
-    baseVFS._rename(session, cutPath(from), cutPath(to), comp)
-
-  override def _backup(session: Object, path: String, comp: Component) =
-    baseVFS._backup(session, cutPath(path), comp)
+  override def _createOutputStream(session: Object, path: String, comp: Component) =
+    new VFS.OutputConverter(base._createOutputStream(session, platform_path(path), comp))
 
   override def _saveComplete(session: Object, buffer: Buffer, path: String, comp: Component) =
-    baseVFS._saveComplete(session, buffer, cutPath(path), comp)
+    base._saveComplete(session, buffer, platform_path(path), comp)
 }