--- a/src/Pure/PIDE/resources.scala Sun Jan 08 14:46:04 2017 +0100
+++ b/src/Pure/PIDE/resources.scala Sun Jan 08 16:47:53 2017 +0100
@@ -145,13 +145,6 @@
start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
with_thy_reader(name, check_thy_reader(qualifier, name, _, start, strict))
- def check_file(file: String): Boolean =
- try {
- if (Url.is_wellformed(file)) Url.is_readable(file)
- else (new JFile(file)).isFile
- }
- catch { case ERROR(_) => false }
-
/* special header */