# HG changeset patch
# User wenzelm
# Date 1343415241 -7200
# Node ID 35c47932584c22c0176b0560a12a98dd02894035
# Parent  af91cd2301ba00f6adbccd943645b08e1bc8778e
even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);

diff -r af91cd2301ba -r 35c47932584c src/Pure/PIDE/document.ML
--- 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 =>