diff options
| author | Carst Tankink | 2014-04-10 12:33:42 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-04-10 19:43:08 +0200 |
| commit | f15525ac29af29bedbb04ae12297d67be3ce6475 (patch) | |
| tree | 45936c39365bf3170b4582610b45931c7b46c39e /lib/serialize.ml | |
| parent | 546d47608f944d9463aaf49ec00dee026fe32818 (diff) | |
Have the feedback bus as a backend for dumping globs.
Diffstat (limited to 'lib/serialize.ml')
| -rw-r--r-- | lib/serialize.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/lib/serialize.ml b/lib/serialize.ml index d91f736fd9..c978177793 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -323,6 +323,8 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "globref", [loc; filepath; modpath; ident; ty] -> GlobRef(to_loc loc, to_string filepath, to_string modpath, to_string ident, to_string ty) + | "globdef", [loc; ident; secpath; ty] -> + GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty) | "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s) | "inprogress", [n] -> InProgress (to_int n) | "slavestatus", [ns] -> @@ -342,6 +344,12 @@ let of_feedback_content = function of_string modpath; of_string ident; of_string ty ] + | GlobDef(loc, ident, secpath, ty) -> + constructor "feedback_content" "globdef" [ + of_loc loc; + of_string ident; + of_string secpath; + of_string ty ] | ErrorMsg(loc, s) -> constructor "feedback_content" "errormsg" [of_loc loc; of_string s] | InProgress n -> constructor "feedback_content" "inprogress" [of_int n] |