diff options
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] |