src/Pure/PIDE/document.ML
changeset 48735 35c47932584c
parent 48707 ba531af91148
child 48755 393a37003851
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Aug 08 14:30:27 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 27 20:54:01 2012 +0200
     1.3 @@ -378,8 +378,8 @@
     1.4      (* FIXME provide files via Scala layer, not master_dir *)
     1.5      val (dir, header) = get_header node;
     1.6      val master_dir =
     1.7 -      (case Url.explode dir of
     1.8 -        Url.File path => path
     1.9 +      (case try Url.explode dir of
    1.10 +        SOME (Url.File path) => path
    1.11        | _ => Path.current);
    1.12      val parents =
    1.13        #imports header |> map (fn import =>