changeset 48409 | 0d2114eb412a |
parent 46938 | cda018294515 |
child 48422 | 9613780a805b |
--- a/src/Pure/Thy/thy_load.scala Fri Jul 20 21:05:47 2012 +0200 +++ b/src/Pure/Thy/thy_load.scala Fri Jul 20 22:29:25 2012 +0200 @@ -7,7 +7,7 @@ package isabelle -import java.io.File +import java.io.{File => JFile} @@ -31,7 +31,7 @@ def read_header(name: Document.Node.Name): Thy_Header = { - val file = new File(name.node) + val file = new JFile(name.node) if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) Thy_Header.read(file) }