# HG changeset patch
# User wenzelm
# Date 1295009887 -3600
# Node ID bd0bebf93fa62fcceefe29d42b9672a10c520c3f
# Parent  1fa4725c4656bce67605cc05e02819616c21249e
Thy_Load.begin_theory: maintain source specification of imports;
Thy_Info.register_thy: reconstruct deps using original imports (important for ProofGeneral.inform_file_processed);

diff -r 1fa4725c4656 -r bd0bebf93fa6 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Jan 13 23:50:16 2011 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Jan 14 13:58:07 2011 +0100
@@ -225,12 +225,12 @@
     val _ = kill_thy name;
     val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
 
-    val {master = (thy_path, _), ...} = deps;
+    val {master = (thy_path, _), imports} = 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 _ =
-      Thy_Load.begin_theory dir name parent_thys uses
+      Thy_Load.begin_theory dir name imports parent_thys uses
       |> Present.begin_theory update_time dir uses;
 
     val (after_load, theory) = Outer_Syntax.load_thy name init pos text;
@@ -324,7 +324,7 @@
     val _ = kill_thy name;
     val _ = use_thys_wrt dir imports;
     val parent_thys = map (get_theory o base_name) imports;
-  in Thy_Load.begin_theory dir name parent_thys uses end;
+  in Thy_Load.begin_theory dir name imports parent_thys uses end;
 
 
 (* register theory *)
@@ -334,7 +334,8 @@
     val name = Context.theory_name theory;
     val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
     val parents = map Context.theory_name (Theory.parents_of theory);
-    val deps = make_deps master parents;
+    val imports = Thy_Load.imports_of theory;
+    val deps = make_deps master imports;
   in
     NAMED_CRITICAL "Thy_Info" (fn () =>
      (kill_thy name;
diff -r 1fa4725c4656 -r bd0bebf93fa6 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Thu Jan 13 23:50:16 2011 +0100
+++ b/src/Pure/Thy/thy_load.ML	Fri Jan 14 13:58:07 2011 +0100
@@ -13,6 +13,7 @@
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
   val master_directory: theory -> Path.T
+  val imports_of: theory -> string list
   val provide: Path.T * (Path.T * file_ident) -> theory -> theory
   val legacy_show_path: unit -> string list
   val legacy_add_path: string -> unit
@@ -28,7 +29,7 @@
   val provide_file: Path.T -> theory -> theory
   val use_ml: Path.T -> unit
   val exec_ml: Path.T -> generic_theory -> generic_theory
-  val begin_theory: Path.T -> string -> theory list -> (Path.T * bool) list -> theory
+  val begin_theory: Path.T -> string -> string list -> theory list -> (Path.T * bool) list -> theory
 end;
 
 structure Thy_Load: THY_LOAD =
@@ -83,40 +84,42 @@
 
 type files =
  {master_dir: Path.T,  (*master directory of theory source*)
+  imports: string list,  (*source specification of imports*)
   required: Path.T list,  (*source path*)
   provided: (Path.T * (Path.T * file_ident)) list};  (*source path, physical path, identifier*)
 
-fun make_files (master_dir, required, provided): files =
- {master_dir = master_dir, required = required, provided = provided};
+fun make_files (master_dir, imports, required, provided): files =
+ {master_dir = master_dir, imports = imports, required = required, provided = provided};
 
 structure Files = Theory_Data
 (
   type T = files;
-  val empty = make_files (Path.current, [], []);
+  val empty = make_files (Path.current, [], [], []);
   fun extend _ = empty;
   fun merge _ = empty;
 );
 
 fun map_files f =
-  Files.map (fn {master_dir, required, provided} =>
-    make_files (f (master_dir, required, provided)));
+  Files.map (fn {master_dir, imports, required, provided} =>
+    make_files (f (master_dir, imports, required, provided)));
 
 
 val master_directory = #master_dir o Files.get;
+val imports_of = #imports o Files.get;
 
-fun master dir = map_files (fn _ => (dir, [], []));
+fun put_deps dir imports = map_files (fn _ => (dir, imports, [], []));
 
 fun require src_path =
-  map_files (fn (master_dir, required, provided) =>
+  map_files (fn (master_dir, imports, required, provided) =>
     if member (op =) required src_path then
       error ("Duplicate source file dependency: " ^ Path.implode src_path)
-    else (master_dir, src_path :: required, provided));
+    else (master_dir, imports, src_path :: required, provided));
 
 fun provide (src_path, path_id) =
-  map_files (fn (master_dir, required, provided) =>
+  map_files (fn (master_dir, imports, required, provided) =>
     if AList.defined (op =) provided src_path then
       error ("Duplicate resolution of source file dependency: " ^ Path.implode src_path)
-    else (master_dir, required, (src_path, path_id) :: provided));
+    else (master_dir, imports, required, (src_path, path_id) :: provided));
 
 
 (* maintain default paths *)
@@ -251,9 +254,9 @@
 
 (* begin theory *)
 
-fun begin_theory dir name parents uses =
+fun begin_theory dir name imports parents uses =
   Theory.begin_theory name parents
-  |> master dir
+  |> put_deps dir imports
   |> fold (require o fst) uses
   |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
   |> Theory.checkpoint;