src/Pure/PIDE/resources.scala
changeset 65494 88e6442c3150
parent 65489 f3076367f4a8
child 65498 2af863e28204
     1.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 17 15:23:51 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 17 16:13:14 2017 +0200
     1.3 @@ -98,9 +98,7 @@
     1.4  
     1.5    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
     1.6    {
     1.7 -    val path = Path.explode(name.node)
     1.8 -    if (!path.is_file) error("No such file: " + path.toString)
     1.9 -
    1.10 +    val path = File.check_file(Path.explode(name.node))
    1.11      val reader = Scan.byte_reader(path.file)
    1.12      try { f(reader) } finally { reader.close }
    1.13    }