# HG changeset patch
# User wenzelm
# Date 1332262894 -3600
# Node ID b32e6de4a39b1cddb1f6de774a9cecbd0a587da4
# Parent  7be54568efa12b5cee053c7a8f5b4dce3fb9395a
minimalistic support for remote URLs: no master dir here;

diff -r 7be54568efa1 -r b32e6de4a39b src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Mar 20 13:53:09 2012 +0100
+++ b/src/Pure/PIDE/document.ML	Tue Mar 20 18:01:34 2012 +0100
@@ -445,7 +445,11 @@
 fun init_theory deps node =
   let
     (* FIXME provide files via Scala layer, not master_dir *)
-    val (master_dir, header) = Exn.release (get_header node);
+    val (dir, header) = Exn.release (get_header node);
+    val master_dir =
+      (case Url.explode dir of
+        Url.File path => path
+      | _ => Path.current);
     val parents =
       #imports header |> map (fn import =>
         (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
@@ -453,7 +457,7 @@
         | NONE =>
             get_theory (Position.file_only import)
               (snd (Future.join (the (AList.lookup (op =) deps import))))));
-  in Thy_Load.begin_theory (Path.explode master_dir) header parents end;
+  in Thy_Load.begin_theory master_dir header parents end;
 
 in