1.1 --- a/src/Pure/Thy/thy_load.scala	Thu Aug 16 14:25:58 2012 +0200
     1.2 +++ b/src/Pure/Thy/thy_load.scala	Thu Aug 16 15:40:26 2012 +0200
     1.3 @@ -43,9 +43,9 @@
     1.4  
     1.5    def read_header(name: Document.Node.Name): Thy_Header =
     1.6    {
     1.7 -    val file = new JFile(name.node)
     1.8 -    if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
     1.9 -    Thy_Header.read(file)
    1.10 +    val path = Path.explode(name.node)
    1.11 +    if (!path.is_file) error("No such file: " + path.toString)
    1.12 +    Thy_Header.read(path.file)
    1.13    }
    1.14  
    1.15