When loading libraries, feed back dependencies.

These dependencies between files can be used by UIs to guide compilation
and reloading of files.

FileDependency (Some "/foo.v", "/bar.v")  means foo depends on bar.
FileDependency (None, "/bar.v") means the current file depends on bar.

3 files changed, 22 insertions, 10 deletions

diff --git a/lib/feedback.ml b/lib/feedback.ml
index 14a1861e8b..eca9b959f4 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -69,6 +69,7 @@ type feedback_content =
   | ProcessingInMaster
   | Goals of Loc.t * string
   | StructuredGoals of Loc.t * xml
+  | FileDependency of string option * string
   | FileLoaded of string * string
   | Message of message
 
@@ -95,8 +96,10 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
        SlaveStatus(n,s)
   | "goals", [loc;s] -> Goals (to_loc loc, to_string s)
   | "structuredgoals", [loc;x]-> StructuredGoals (to_loc loc, x)
+  | "filedependency", [from; dep] ->
+      FileDependency (to_option to_string from, to_string dep)
   | "fileloaded", [dirpath; filename] ->
-       FileLoaded(to_string dirpath, to_string filename)
+      FileLoaded (to_string dirpath, to_string filename)
   | "message", [m] -> Message (to_message m)
   | _ -> raise Marshal_error)
 let of_feedback_content = function
@@ -128,7 +131,11 @@ let of_feedback_content = function
       constructor "feedback_content" "goals" [of_loc loc;of_string s]
   | StructuredGoals (loc, x) ->
       constructor "feedback_content" "structuredgoals" [of_loc loc; x]
-  | FileLoaded(dirpath, filename) ->
+  | FileDependency (from, depends_on) ->
+      constructor "feedback_content" "filedependency" [
+        of_option of_string from;
+        of_string depends_on]
+  | FileLoaded (dirpath, filename) ->
       constructor "feedback_content" "fileloaded" [
         of_string dirpath;
         of_string filename ]
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 775f71e9e5..d6d77b7cc4 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -44,6 +44,7 @@ type feedback_content =
   | ProcessingInMaster
   | Goals of Loc.t * string
   | StructuredGoals of Loc.t * xml
+  | FileDependency of string option * string
   | FileLoaded of string * string
   | Message of message
 
diff --git a/library/library.ml b/library/library.ml
index ceadb3ace0..97c4165569 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -402,7 +402,11 @@ let intern_from_file f =
 
 module DPMap = Map.Make(DirPath)
 
-let rec intern_library (needed, contents) (dir, f) =
+let deps_to_string deps =
+  Array.fold_left (fun s (n, _) -> s^"\n  - "^(DirPath.to_string n)) "" deps
+
+let rec intern_library (needed, contents) (dir, f) from =
+  Pp.feedback(Feedback.FileDependency (from, f));
   (* Look if in the current logical environment *)
   try find_library dir, (needed, contents)
   with Not_found ->
@@ -417,14 +421,14 @@ let rec intern_library (needed, contents) (dir, f) =
        pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
        spc() ++ pr_dirpath dir);
   Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f));
-  m, intern_library_deps (needed, contents) dir m
+  m, intern_library_deps (needed, contents) dir m (Some f)
 
-and intern_library_deps libs dir m =
-  let needed, contents = Array.fold_left (intern_mandatory_library dir) libs m.library_deps in
+and intern_library_deps libs dir m from =
+  let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in
   (dir :: needed, DPMap.add dir m contents )
 
-and intern_mandatory_library caller libs (dir,d) =
-  let m, libs = intern_library libs (try_locate_absolute_library dir) in
+and intern_mandatory_library caller from libs (dir,d) =
+  let m, libs = intern_library libs (try_locate_absolute_library dir) from in
   if not (Safe_typing.digest_match ~actual:m.library_digests ~required:d) then
     errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^
       ".vo makes inconsistent assumptions over library " ^
@@ -432,7 +436,7 @@ and intern_mandatory_library caller libs (dir,d) =
   libs
 
 let rec_intern_library libs mref =
-  let _, libs = intern_library libs mref in
+  let _, libs = intern_library libs mref None in
   libs
 
 let check_library_short_name f dir = function
@@ -458,7 +462,7 @@ let rec_intern_by_filename_only id f =
       m.library_name, []
     end
  else
-    let needed, contents = intern_library_deps ([], DPMap.empty) m.library_name m in
+    let needed, contents = intern_library_deps ([], DPMap.empty) m.library_name m (Some f) in
     let needed = List.map (fun dir -> dir, DPMap.find dir contents) needed in
     m.library_name, needed