simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
tuned;

--- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Tue Aug 03 08:23:08 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Tue Aug 03 15:53:36 2010 +0200
@@ -80,9 +80,9 @@
                NONE => (NONE, NONE)
              | SOME fname =>
                let val path = Path.explode fname in
-                 case Thy_Load.test_file Path.current path of
-                   SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
-                 | NONE => (NONE, SOME fname)
+                 if can (Thy_Load.check_file [Path.current]) path
+                 then (SOME (PgipTypes.pgipurl_of_path path), NONE)
+                 else (NONE, SOME fname)
                end);
     in
         { descr=descr, url=url, line=line, column=column, char=NONE, length=NONE }

--- a/src/Pure/Thy/present.ML	Tue Aug 03 08:23:08 2010 +0200
+++ b/src/Pure/Thy/present.ML	Tue Aug 03 15:53:36 2010 +0200
@@ -462,7 +462,7 @@
 
     val files_html = files |> map (fn (raw_path, loadit) =>
       let
-        val path = #1 (Thy_Load.check_file dir raw_path);
+        val path = #1 (Thy_Load.check_file [dir] raw_path);
         val base = Path.base path;
         val base_html = html_ext base;
         val _ = add_file (Path.append html_prefix base_html,

--- a/src/Pure/Thy/thy_load.ML	Tue Aug 03 08:23:08 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Aug 03 15:53:36 2010 +0200
@@ -22,8 +22,7 @@
   val master_directory: theory -> Path.T
   val require: Path.T -> theory -> theory
   val provide: Path.T * (Path.T * File.ident) -> theory -> theory
-  val test_file: Path.T -> Path.T -> (Path.T * File.ident) option
-  val check_file: Path.T -> Path.T -> Path.T * File.ident
+  val check_file: Path.T list -> Path.T -> Path.T * File.ident
   val check_thy: Path.T -> string -> Path.T * File.ident
   val deps_thy: Path.T -> string ->
    {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
@@ -110,45 +109,37 @@
 
 (* check files *)
 
-local
-
-exception NOT_FOUND of Path.T list * Path.T;
-
-fun try_file dir src_path =
+fun get_file dirs src_path =
   let
-    val prfxs = search_path dir src_path;
     val path = Path.expand src_path;
     val _ = Path.is_current path andalso error "Bad file specification";
-    val result =
-      prfxs |> get_first (fn prfx =>
-        let val full_path = File.full_path (Path.append prfx path)
-        in Option.map (pair full_path) (File.ident full_path) end);
   in
-    (case result of
-      SOME res => res
-    | NONE => raise NOT_FOUND (prfxs, path))
+    dirs |> get_first (fn dir =>
+      let val full_path = File.full_path (Path.append dir path) in
+        (case File.ident full_path of
+          NONE => NONE
+        | SOME id => SOME (full_path, id))
+      end)
   end;
 
-in
-
-fun test_file dir file =
-  SOME (try_file dir file) handle NOT_FOUND _ => NONE;
+fun check_file dirs file =
+  (case get_file dirs file of
+    SOME path_id => path_id
+  | NONE => error ("Could not find file " ^ quote (Path.implode file) ^
+      "\nin " ^ commas_quote (map Path.implode dirs)));
 
-fun check_file dir file =
-  try_file dir file handle NOT_FOUND (prfxs, path) =>
-    error ("Could not find file " ^ quote (Path.implode path) ^
-      "\nin " ^ commas_quote (map Path.implode prfxs));
-
-fun check_thy dir name = check_file dir (Thy_Header.thy_path name);
-
-end;
+fun check_thy master_dir name =
+  let
+    val thy_file = Thy_Header.thy_path name;
+    val dirs = search_path master_dir thy_file;
+  in check_file dirs thy_file end;
 
 
 (* theory deps *)
 
-fun deps_thy dir name =
+fun deps_thy master_dir name =
   let
-    val master as (thy_path, _) = check_thy dir name;
+    val master as (thy_path, _) = check_thy master_dir name;
     val text = File.read thy_path;
     val (name', imports, uses) = Thy_Header.read (Path.position thy_path) text;
     val _ = Thy_Header.consistent_name name name';
@@ -179,7 +170,7 @@
   let
     val {master_dir, provided, ...} = Files.get thy;
     fun current (src_path, (_, id)) =
-      (case test_file master_dir src_path of
+      (case get_file [master_dir] src_path of
         NONE => false
       | SOME (_, id') => id = id');
   in can check_loaded thy andalso forall current provided end;
@@ -190,15 +181,15 @@
 (* provide files *)
 
 fun provide_file src_path thy =
-  provide (src_path, check_file (master_directory thy) src_path) thy;
+  provide (src_path, check_file [master_directory thy] src_path) thy;
 
 fun use_ml src_path =
   if is_none (Context.thread_data ()) then
-    ML_Context.eval_file (#1 (check_file Path.current src_path))
+    ML_Context.eval_file (#1 (check_file [Path.current] src_path))
   else
     let
       val thy = ML_Context.the_global_context ();
-      val (path, id) = check_file (master_directory thy) src_path;
+      val (path, id) = check_file [master_directory thy] src_path;
 
       val _ = ML_Context.eval_file path;
       val _ = Context.>> Local_Theory.propagate_ml_env;