# HG changeset patch
# User wenzelm
# Date 1280845293 -7200
# Node ID 3de75ca6f1667db0d85b07c58ec9058a6fa319b8
# Parent  987680d2e77d88889a5821a198207c81d3681111
load_thy: refer to physical master directory (not accumulated source import directory) and enable loading files relatively to that;

diff -r 987680d2e77d -r 3de75ca6f166 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Aug 03 15:53:36 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Aug 03 16:21:33 2010 +0200
@@ -238,12 +238,13 @@
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy initiators update_time (deps: deps) text dir name parent_thys =
+fun load_thy initiators update_time (deps: deps) text name parent_thys =
   let
     val _ = kill_thy name;
     val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
 
     val {master = (thy_path, _), ...} = deps;
+    val dir = Path.dir thy_path;
     val pos = Path.position thy_path;
     val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
     fun init () =
@@ -317,7 +318,7 @@
                   let
                     val text = (case opt_text of SOME text => text | NONE => File.read thy_path);
                     val update_time = serial ();
-                  in Task (parent_names, load_thy initiators update_time dep text dir' name) end);
+                  in Task (parent_names, load_thy initiators update_time dep text name) end);
         in (all_current, new_entry name parent_names task tasks') end)
   end;