simplified Thy_Load.provide: do not store full path;

--- a/src/Pure/Thy/thy_load.ML	Wed Aug 22 23:45:49 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Aug 23 11:58:10 2012 +0200
@@ -8,7 +8,7 @@
 sig
   val master_directory: theory -> Path.T
   val imports_of: theory -> string list
-  val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
+  val provide: Path.T * SHA1.digest -> theory -> theory
   val check_file: Path.T -> Path.T -> Path.T
   val thy_path: Path.T -> Path.T
   val check_thy: Thy_Header.keywords -> Path.T -> string ->
@@ -36,7 +36,7 @@
 type files =
  {master_dir: Path.T,  (*master directory of theory source*)
   imports: string list,  (*source specification of imports*)
-  provided: (Path.T * (Path.T * SHA1.digest)) list};  (*source path, physical path, digest*)
+  provided: (Path.T * SHA1.digest) list};  (*source path, digest*)
 
 fun make_files (master_dir, imports, provided): files =
  {master_dir = master_dir, imports = imports, provided = provided};
@@ -59,11 +59,11 @@
 
 fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
 
-fun provide (src_path, path_id) =
+fun provide (src_path, id) =
   map_files (fn (master_dir, imports, provided) =>
     if AList.defined (op =) provided src_path then
       error ("Duplicate use of source file: " ^ Path.print src_path)
-    else (master_dir, imports, (src_path, path_id) :: provided));
+    else (master_dir, imports, (src_path, id) :: provided));
 
 
 (* inlined files *)
@@ -178,15 +178,17 @@
 
 fun use_file src_path thy =
   let
-    val (path_id, text) = load_file thy src_path;
-    val thy' = provide (src_path, path_id) thy;
+    val ((_, id), text) = load_file thy src_path;
+    val thy' = provide (src_path, id) thy;
   in (text, thy') end;
 
-val loaded_files = map (#1 o #2) o #provided o Files.get;
+fun loaded_files thy =
+  let val {master_dir, provided, ...} = Files.get thy
+  in map (File.full_path master_dir o #1) provided end;
 
 fun load_current thy =
   #provided (Files.get thy) |>
-    forall (fn (src_path, (_, id)) =>
+    forall (fn (src_path, id) =>
       (case try (load_file thy) src_path of
         NONE => false
       | SOME ((_, id'), _) => id = id'));
@@ -208,7 +210,7 @@
       val _ = eval_file path text;
       val _ = Context.>> Local_Theory.propagate_ml_env;
 
-      val provide = provide (src_path, (path, id));
+      val provide = provide (src_path, id);
       val _ = Context.>> (Context.mapping provide (Local_Theory.background_theory provide));
     in () end;
 

--- a/src/Pure/pure_syn.ML	Wed Aug 22 23:45:49 2012 +0200
+++ b/src/Pure/pure_syn.ML	Thu Aug 23 11:58:10 2012 +0200
@@ -22,8 +22,8 @@
       >> (fn (name, files) => Toplevel.generic_theory (fn gthy =>
         let
           val src_path = Path.explode name;
-          val (dir, [(txt, pos)]) = files (Context.theory_of gthy);
-          val provide = Thy_Load.provide (src_path, (File.full_path dir src_path, SHA1.digest txt));
+          val (_, [(txt, pos)]) = files (Context.theory_of gthy);
+          val provide = Thy_Load.provide (src_path, SHA1.digest txt);
         in
           gthy
           |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)