diff options
author | 2014-10-09 15:39:08 +0200 | |
---|---|---|
committer | 2014-10-13 18:13:21 +0200 | |
commit | 0253fc47be156d0d87cccda32c5bb90bc37960da (patch) | |
tree | f5eac948b0a6eddceef5403185e5fb9760b8e628 /lib | |
parent | e1ea8a70094dfed28223d02dfca5d768737d4421 (diff) |
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.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/feedback.ml | 11 | ||||
-rw-r--r-- | lib/feedback.mli | 1 |
2 files changed, 10 insertions, 2 deletions
diff --git a/lib/feedback.ml b/lib/feedback.ml index 14a1861e8..eca9b959f 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 775f71e9e..d6d77b7cc 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 |