improved support for external URLs, based on standard Java network operations;
authorwenzelm
Wed Apr 09 23:22:58 2014 +0200 (2014-04-09)
changeset 56502db2836f65d42
parent 56501 5fda9e5c5874
child 56503 9e23fafe4037
improved support for external URLs, based on standard Java network operations;
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 09 23:04:20 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 09 23:22:58 2014 +0200
     1.3 @@ -10,10 +10,10 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import java.io.{File => JFile, IOException, ByteArrayOutputStream}
     1.8 +import java.io.{File => JFile, ByteArrayOutputStream}
     1.9  import javax.swing.text.Segment
    1.10  
    1.11 -import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
    1.12 +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
    1.13  import org.gjt.sp.jedit.MiscUtilities
    1.14  import org.gjt.sp.jedit.{jEdit, View, Buffer}
    1.15  import org.gjt.sp.jedit.bufferio.BufferIORequest
    1.16 @@ -45,6 +45,7 @@
    1.17    {
    1.18      val path = source_path.expand
    1.19      if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
    1.20 +    else if (path.is_current) dir
    1.21      else {
    1.22        val vfs = VFSManager.getVFSForPath(dir)
    1.23        if (vfs.isInstanceOf[FileVFS])
    1.24 @@ -54,42 +55,32 @@
    1.25      }
    1.26    }
    1.27  
    1.28 -  override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
    1.29 +  override def with_thy_text[A](name: Document.Node.Name, consume: CharSequence => A): A =
    1.30    {
    1.31      Swing_Thread.now {
    1.32        JEdit_Lib.jedit_buffer(name) match {
    1.33          case Some(buffer) =>
    1.34            JEdit_Lib.buffer_lock(buffer) {
    1.35 -            Some(f(buffer.getSegment(0, buffer.getLength)))
    1.36 +            Some(consume(buffer.getSegment(0, buffer.getLength)))
    1.37            }
    1.38          case None => None
    1.39        }
    1.40      } getOrElse {
    1.41 -      val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
    1.42 -      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    1.43 -      f(File.read(file))
    1.44 +      if (Url.is_wellformed(name.node)) consume(Url.read(name.node))
    1.45 +      else {
    1.46 +        val file = new JFile(name.node)
    1.47 +        if (file.isFile) consume(File.read(file))
    1.48 +        else error("No such file: " + quote(file.toString))
    1.49 +      }
    1.50      }
    1.51    }
    1.52  
    1.53 -  def check_file(view: View, path: String): Boolean =
    1.54 -  {
    1.55 -    val vfs = VFSManager.getVFSForPath(path)
    1.56 -    val session = vfs.createVFSSession(path, view)
    1.57 -
    1.58 +  def check_file(view: View, file: String): Boolean =
    1.59      try {
    1.60 -      session != null && {
    1.61 -        try {
    1.62 -          val file = vfs._getFile(session, path, view)
    1.63 -          file != null && file.isReadable && file.getType == VFSFile.FILE
    1.64 -        }
    1.65 -        catch { case _: IOException => false }
    1.66 -      }
    1.67 +      if (Url.is_wellformed(file)) Url.is_readable(file)
    1.68 +      else (new JFile(file)).isFile
    1.69      }
    1.70 -    finally {
    1.71 -      try { vfs._endVFSSession(session, view) }
    1.72 -      catch { case _: IOException => }
    1.73 -    }
    1.74 -  }
    1.75 +    catch { case ERROR(_) => false }
    1.76  
    1.77  
    1.78    /* file content */