src/Pure/PIDE/document.ML
changeset 48735 35c47932584c
parent 48707 ba531af91148
child 48755 393a37003851
--- 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 =>