src/Pure/PIDE/resources.scala
changeset 64835 fd1efd6dd385
parent 64826 c97296294f6d
child 64839 842163abfc0d
     1.1 --- a/src/Pure/PIDE/resources.scala	Sun Jan 08 14:46:04 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sun Jan 08 16:47:53 2017 +0100
     1.3 @@ -145,13 +145,6 @@
     1.4        start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
     1.5      with_thy_reader(name, check_thy_reader(qualifier, name, _, start, strict))
     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    /* special header */
    1.16