minimalistic support for remote URLs: no master dir here;
authorwenzelm
Tue, 20 Mar 2012 18:01:34 +0100
changeset 47927b32e6de4a39b
parent 47921 7be54568efa1
child 47928 12423b36fcc4
minimalistic support for remote URLs: no master dir here;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Mar 20 13:53:09 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Mar 20 18:01:34 2012 +0100
     1.3 @@ -445,7 +445,11 @@
     1.4  fun init_theory deps node =
     1.5    let
     1.6      (* FIXME provide files via Scala layer, not master_dir *)
     1.7 -    val (master_dir, header) = Exn.release (get_header node);
     1.8 +    val (dir, header) = Exn.release (get_header node);
     1.9 +    val master_dir =
    1.10 +      (case Url.explode dir of
    1.11 +        Url.File path => path
    1.12 +      | _ => Path.current);
    1.13      val parents =
    1.14        #imports header |> map (fn import =>
    1.15          (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
    1.16 @@ -453,7 +457,7 @@
    1.17          | NONE =>
    1.18              get_theory (Position.file_only import)
    1.19                (snd (Future.join (the (AList.lookup (op =) deps import))))));
    1.20 -  in Thy_Load.begin_theory (Path.explode master_dir) header parents end;
    1.21 +  in Thy_Load.begin_theory master_dir header parents end;
    1.22  
    1.23  in
    1.24