# HG changeset patch
# User wenzelm
# Date 1492438394 -7200
# Node ID 88e6442c31509b04562a2b4cef36133056a874c9
# Parent  4729318d3fc38cd59e9c14cdc9f84573c0e3f51a
tuned;

diff -r 4729318d3fc3 -r 88e6442c3150 src/Pure/PIDE/resources.scala
--- 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 }
   }