even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);
authorwenzelm
Fri Jul 27 20:54:01 2012 +0200 (2012-07-27)
changeset 4873535c47932584c
parent 48734 af91cd2301ba
child 48736 292b97e17fb7
even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);
src/Pure/PIDE/document.ML
     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 =>