more robust multi-platform support;

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