src/Pure/Thy/thy_load.ML

 signature THY_LOAD =
 sig
   val master_directory: theory -> Path.T
   val imports_of: theory -> string list
   val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
-  val check_file: Path.T -> Path.T -> Path.T * SHA1.digest
-  val check_thy: Path.T -> string -> Path.T * SHA1.digest
-  val deps_thy: Path.T -> string ->
-   {master: Path.T * SHA1.digest, text: string, imports: string list, uses: Path.T list}
+  val check_file: Path.T -> Path.T -> Path.T
+  val check_thy: Path.T -> string ->
+    {master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list}
   val loaded_files: theory -> Path.T list
   val all_current: theory -> bool
   val provide_file: Path.T -> theory -> theory
   val use_ml: Path.T -> unit
   val exec_ml: Path.T -> generic_theory -> generic_theory

     else (master_dir, imports, required, (src_path, path_id) :: provided));
 
 
 (* check files *)
 
-fun get_file dir src_path =
+fun check_file dir file = File.check_file (File.full_path dir file);
+
+fun digest_file dir file =
   let
-    val path = Path.expand src_path;
-    val _ = Path.is_current path andalso error "Bad file specification";
-    val full_path = File.full_path (Path.append dir path);
-  in
-    if File.exists full_path
-    then SOME (full_path, SHA1.digest (File.read full_path))
-    else NONE
-  end;
-
-fun check_file dir file =
-  (case get_file dir file of
-    SOME path_id => path_id
-  | NONE => error ("Could not find file " ^ Path.print file ^ "\nin " ^ Path.print dir));
+    val full_path = check_file dir file;
+    val id = SHA1.digest (File.read full_path);
+  in (full_path, id) end;
 
 fun check_thy dir name =
-  check_file dir (Thy_Header.thy_path name);
-
-
-(* theory deps *)
-
-fun deps_thy master_dir name =
   let
-    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 master_file = check_file dir (Thy_Header.thy_path name);
+    val text = File.read master_file;
+    val (name', imports, uses) =
+      if name = Context.PureN then (Context.PureN, [], [])
+      else Thy_Header.read (Path.position master_file) text;
     val _ = Thy_Header.consistent_name name name';
-    val uses = map (Path.explode o #1) uses;
-  in {master = master, text = text, imports = imports, uses = uses} end;
-
+  in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end;
 
 
 (* loaded files *)
 
 val loaded_files = map (#1 o #2) o #provided o Files.get;

 
 fun all_current thy =
   let
     val {master_dir, provided, ...} = Files.get thy;
     fun current (src_path, (_, id)) =
-      (case get_file master_dir src_path of
+      (case try (digest_file master_dir) src_path of
         NONE => false
       | SOME (_, id') => id = id');
   in can check_loaded thy andalso forall current provided end;
 
 val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE))));
 
 
 (* provide files *)
 
 fun provide_file src_path thy =
-  provide (src_path, check_file (master_directory thy) src_path) thy;
+  provide (src_path, digest_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 (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) = digest_file (master_directory thy) src_path;
 
       val _ = ML_Context.eval_file path;
       val _ = Context.>> Local_Theory.propagate_ml_env;
 
       val provide = provide (src_path, (path, id));