# HG changeset patch
# User wenzelm
# Date 1345124426 -7200
# Node ID 8791d106e30b70792401c138a062dceed6bc7868
# Parent  b19ba23e70c5779063fa37db1c9b9076766bb64a
more robust multi-platform support;

diff -r b19ba23e70c5 -r 8791d106e30b src/Pure/Thy/thy_load.scala
--- 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)
   }