use Plugin.self.symbols;
authorwenzelm
Sun, 21 Dec 2008 21:43:41 +0100
changeset 34436 a77cfbe18a31
parent 34435 926272164bff
child 34437 4eb1b75c746d
use Plugin.self.symbols; tuned;
src/Tools/jEdit/src/jedit/VFS.scala
--- a/src/Tools/jEdit/src/jedit/VFS.scala	Sun Dec 21 21:43:41 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/VFS.scala	Sun Dec 21 21:43:41 2008 +0100
@@ -10,34 +10,27 @@
 
 package isabelle.jedit
 
-import java.io.InputStream
-import java.io.OutputStream
-import java.io.ByteArrayInputStream
-import java.io.ByteArrayOutputStream
-import java.io.InputStreamReader
 
+import java.io.{InputStream, OutputStream, ByteArrayInputStream, ByteArrayOutputStream, InputStreamReader}
 import java.awt.Component
 
-import isabelle.Symbol.Interpretation
-
 import org.gjt.sp.jedit.Buffer
 import org.gjt.sp.jedit.View
 import org.gjt.sp.jedit.io
 import org.gjt.sp.jedit.io.VFSFile
 import org.gjt.sp.jedit.io.VFSManager
 
-object VFS {
-  val converter = new Interpretation()
-  
+
+object VFS {  
   val BUFFER_SIZE = 1024
   
-  def inputConverter(in : InputStream) = {
-    val reader = new InputStreamReader(in, "UTF-8")
-    val buffer = new StringBuffer()
+  def input_converter(in: InputStream) = {
+    val reader = new InputStreamReader(in, IsabelleSystem.charset)
+    val buffer = new StringBuilder
     val array = new Array[Char](BUFFER_SIZE)
     
     var finished = false
-    while (! finished) {
+    while (!finished) {
       val length = reader.read(array, 0, array.length)
       if (length == -1)
         finished = true
@@ -45,31 +38,33 @@
         buffer.append(array, 0, length)
     }
 
-    val str = converter.decode(buffer.toString())
-    new ByteArrayInputStream(str.getBytes("UTF-8"))
+    val str = Plugin.self.symbols.decode(buffer.toString)
+    new ByteArrayInputStream(str.getBytes(IsabelleSystem.charset))
   }
   
-  class OutputConverter(out : OutputStream) extends ByteArrayOutputStream {
+  class OutputConverter(out: OutputStream) extends ByteArrayOutputStream {
     override def close() {
-      out.write(converter.encode(new String(buf, 0, count)).getBytes())
+      out.write(Plugin.self.symbols.encode(new String(buf, 0, count)).getBytes)
       out.close()
     }
   }
   
-  def mapFile(vfs : VFS, base : VFSFile) =
+  def map_file(vfs: VFS, base: VFSFile) =
     if (base == null) null else new File(vfs, base)
   
-  class File(vfs : VFS, base : VFSFile) extends VFSFile {
+  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) =
+    override def getExtendedAttribute(name: String) =
       base.getExtendedAttribute(name)
 
-    override def getIcon(expanded : Boolean, openBuffer : Boolean) = 
+    override def getIcon(expanded: Boolean, openBuffer: Boolean) = 
       base.getIcon(expanded, openBuffer)
 
     override def getLength() = 
@@ -90,7 +85,7 @@
     override def getVFS() =
       vfs
 
-    override def isBinary(session : Object) =
+    override def isBinary(session: Object) =
       base.isBinary(session)
 
     override def isHidden() =
@@ -102,43 +97,44 @@
     override def isWriteable() =
       base.isWriteable()
 
-    override def setDeletePath(path : String) =
+    override def setDeletePath(path: String) =
       base.setDeletePath(path)
     
-    override def setHidden(hidden : Boolean) =
+    override def setHidden(hidden: Boolean) =
       base.setHidden(hidden)
       
-    override def setLength(length : Long) =
+    override def setLength(length: Long) =
       base.setLength(length)
       
-    override def setName(name : String) =
+    override def setName(name: String) =
       base.setName(name)
       
-    override def setPath(path : String) =
+    override def setPath(path: String) =
       base.setPath(path)
       
-    override def setReadable(readable : Boolean) =
+    override def setReadable(readable: Boolean) =
       base.setReadable(readable)
       
-    override def setWriteable(writeable : Boolean) =
+    override def setWriteable(writeable: Boolean) =
       base.setWriteable(writeable)
       
-    override def setSymlinkPath(symlinkPath : String) =
+    override def setSymlinkPath(symlinkPath: String) =
       base.setSymlinkPath(symlinkPath)
       
-    override def setType(fType : Int) =
+    override def setType(fType: Int) =
       base.setType(fType)
-  } 
-  
+  }  
 }
 
-class VFS extends io.VFS("isabelle", VFSManager.getVFSForProtocol("file").getCapabilities()) {
-  private var baseVFS = VFSManager.getVFSForProtocol("file") 
+
+class VFS extends io.VFS("isabelle", VFSManager.getVFSForProtocol("file").getCapabilities) {
+  private var baseVFS = VFSManager.getVFSForProtocol("file")
 
-  private def cutPath(path : String) = 
-    if (path.startsWith(Plugin.VFS_PREFIX)) path.substring(Plugin.VFS_PREFIX.length) else path
+  private def cutPath(path: String) = 
+    if (path.startsWith(Plugin.VFS_PREFIX)) path.substring(Plugin.VFS_PREFIX.length)
+    else path
   
-  override def createVFSSession(path : String, comp : Component) = 
+  override def createVFSSession(path: String, comp: Component) = 
     baseVFS.createVFSSession(cutPath(path), comp)
   
   override def getCapabilities() = 
@@ -147,54 +143,49 @@
   override def getExtendedAttributes() = 
     baseVFS.getExtendedAttributes()
   
-  override def getParentOfPath(path : String) = 
+  override def getParentOfPath(path: String) = 
     Plugin.VFS_PREFIX + baseVFS.getParentOfPath(cutPath(path))
   
-  override def constructPath(parent : String, path : String) = 
+  override def constructPath(parent: String, path: String) = 
     Plugin.VFS_PREFIX + baseVFS.constructPath(cutPath(parent), path)
   
-  override def getFileName(path : String) = 
+  override def getFileName(path: String) = 
     baseVFS.getFileName(path)
   
   override def getFileSeparator() = 
     baseVFS.getFileSeparator()
   
-  override def getTwoStageSaveName(path : String) = 
+  override def getTwoStageSaveName(path: String) = 
     Plugin.VFS_PREFIX + baseVFS.getTwoStageSaveName(cutPath(path))
   
-  override def _canonPath(session : Object, path : String, comp : Component) =
+  override def _canonPath(session: Object, path: String, comp: Component) =
     Plugin.VFS_PREFIX + baseVFS._canonPath(session, cutPath(path), comp)
   
-  override def _createInputStream(session : Object, path : String,
-                                  ignoreErrors : Boolean, comp : Component) =
-    VFS.inputConverter(baseVFS._createInputStream(session, cutPath(path), 
-                                                  ignoreErrors, 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) =
+  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) =
+  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.mapFile(this, baseVFS._getFile(session, cutPath(path), comp))
+  override def _getFile(session: Object, path: String, comp: Component) =
+    VFS.map_file(this, baseVFS._getFile(session, cutPath(path), comp))
 
-  override def _listFiles(session : Object, path : String, comp :  Component): Array[VFSFile] =
-    (baseVFS._listFiles(session, cutPath(path), comp)
-            .map(file => VFS.mapFile(this, file)))
+  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) =
+  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) =
+  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 _backup(session: Object, path: String, comp: Component) =
+    baseVFS._backup(session, cutPath(path), comp)
 
-  override def _saveComplete(session : Object, buffer : Buffer, path : String,
-                             comp : Component) =
+  override def _saveComplete(session: Object, buffer: Buffer, path: String, comp: Component) =
     baseVFS._saveComplete(session, buffer, cutPath(path), comp)
 }