src/Pure/PIDE/resources.scala
changeset 59691 f6ff19188842
parent 59689 7968c57ea240
child 59694 d2bb4b5ed862
     1.1 --- a/src/Pure/PIDE/resources.scala	Fri Mar 13 16:09:55 2015 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Fri Mar 13 21:35:48 2015 +0100
     1.3 @@ -110,6 +110,13 @@
     1.4    def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
     1.5      with_thy_reader(name, check_thy_reader(qualifier, name, _))
     1.6  
     1.7 +  def check_file(file: String): Boolean =
     1.8 +    try {
     1.9 +      if (Url.is_wellformed(file)) Url.is_readable(file)
    1.10 +      else (new JFile(file)).isFile
    1.11 +    }
    1.12 +    catch { case ERROR(_) => false }
    1.13 +
    1.14  
    1.15    /* document changes */
    1.16