aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/feedback.ml
diff options
context:
space:
mode:
authorGravatar Carst Tankink <carst.tankink@inria.fr>2014-10-09 15:39:08 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-10-13 18:13:21 +0200
commit0253fc47be156d0d87cccda32c5bb90bc37960da (patch)
treef5eac948b0a6eddceef5403185e5fb9760b8e628 /lib/feedback.ml
parente1ea8a70094dfed28223d02dfca5d768737d4421 (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/feedback.ml')
-rw-r--r--lib/feedback.ml11
1 files changed, 9 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 ]