# HG changeset patch
# User wenzelm
# Date 1211652737 -7200
# Node ID e40f28cdd19bc288b19944ca5cd9f8cf9b273fe4
# Parent  de7738deadfbee8789a6a9a464c319dde82aced5
exported master_directory;

diff -r de7738deadfb -r e40f28cdd19b src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat May 24 20:12:16 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat May 24 20:12:17 2008 +0200
@@ -26,6 +26,7 @@
   val get_theory: string -> theory
   val the_theory: string -> theory -> theory
   val is_finished: string -> bool
+  val master_directory: string -> Path.T
   val loaded_files: string -> Path.T list
   val get_parents: string -> string list
   val touch_child_thys: string -> unit
@@ -153,7 +154,8 @@
 val get_deps = #1 o get_thy;
 fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
 
-fun is_finished name = is_none (get_deps name);
+val is_finished = is_none o get_deps;
+val master_directory = master_dir' o get_deps;
 
 fun loaded_files name =
   (case get_deps name of
@@ -270,10 +272,10 @@
 
 fun provide_file path name =
   let
-    val deps = get_deps name;
+    val dir = master_directory name;
     val _ = check_unfinished error name;
   in
-    (case ThyLoad.check_file (master_dir' deps) path of
+    (case ThyLoad.check_file dir path of
       SOME path_info => change_deps name (provide path name path_info)
     | NONE => error ("Could not find file " ^ quote (Path.implode path)))
   end;