src/Pure/PIDE/resources.scala

--- a/src/Pure/PIDE/resources.scala	Fri Mar 13 16:09:55 2015 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Mar 13 21:35:48 2015 +0100
@@ -110,6 +110,13 @@
   def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
     with_thy_reader(name, check_thy_reader(qualifier, name, _))
 
+  def check_file(file: String): Boolean =
+    try {
+      if (Url.is_wellformed(file)) Url.is_readable(file)
+      else (new JFile(file)).isFile
+    }
+    catch { case ERROR(_) => false }
+
 
   /* document changes */