even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);

--- a/src/Pure/PIDE/document.ML	Wed Aug 08 14:30:27 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Jul 27 20:54:01 2012 +0200
@@ -378,8 +378,8 @@
     (* FIXME provide files via Scala layer, not master_dir *)
     val (dir, header) = get_header node;
     val master_dir =
-      (case Url.explode dir of
-        Url.File path => path
+      (case try Url.explode dir of
+        SOME (Url.File path) => path
       | _ => Path.current);
     val parents =
       #imports header |> map (fn import =>