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