# HG changeset patch
# User wenzelm
# Date 1397078578 -7200
# Node ID db2836f65d429924eb32d835c6a78ff1ed37838f
# Parent  5fda9e5c5874660120792f1aa1c969646e6bb606
improved support for external URLs, based on standard Java network operations;

diff -r 5fda9e5c5874 -r db2836f65d42 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 09 23:04:20 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 09 23:22:58 2014 +0200
@@ -10,10 +10,10 @@
 
 import isabelle._
 
-import java.io.{File => JFile, IOException, ByteArrayOutputStream}
+import java.io.{File => JFile, ByteArrayOutputStream}
 import javax.swing.text.Segment
 
-import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
+import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
 import org.gjt.sp.jedit.MiscUtilities
 import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.bufferio.BufferIORequest
@@ -45,6 +45,7 @@
   {
     val path = source_path.expand
     if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
+    else if (path.is_current) dir
     else {
       val vfs = VFSManager.getVFSForPath(dir)
       if (vfs.isInstanceOf[FileVFS])
@@ -54,42 +55,32 @@
     }
   }
 
-  override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
+  override def with_thy_text[A](name: Document.Node.Name, consume: CharSequence => A): A =
   {
     Swing_Thread.now {
       JEdit_Lib.jedit_buffer(name) match {
         case Some(buffer) =>
           JEdit_Lib.buffer_lock(buffer) {
-            Some(f(buffer.getSegment(0, buffer.getLength)))
+            Some(consume(buffer.getSegment(0, buffer.getLength)))
           }
         case None => None
       }
     } getOrElse {
-      val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
-      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
-      f(File.read(file))
+      if (Url.is_wellformed(name.node)) consume(Url.read(name.node))
+      else {
+        val file = new JFile(name.node)
+        if (file.isFile) consume(File.read(file))
+        else error("No such file: " + quote(file.toString))
+      }
     }
   }
 
-  def check_file(view: View, path: String): Boolean =
-  {
-    val vfs = VFSManager.getVFSForPath(path)
-    val session = vfs.createVFSSession(path, view)
-
+  def check_file(view: View, file: String): Boolean =
     try {
-      session != null && {
-        try {
-          val file = vfs._getFile(session, path, view)
-          file != null && file.isReadable && file.getType == VFSFile.FILE
-        }
-        catch { case _: IOException => false }
-      }
+      if (Url.is_wellformed(file)) Url.is_readable(file)
+      else (new JFile(file)).isFile
     }
-    finally {
-      try { vfs._endVFSSession(session, view) }
-      catch { case _: IOException => }
-    }
-  }
+    catch { case ERROR(_) => false }
 
 
   /* file content */