diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-05 13:39:59 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-06 05:47:47 -0400 |
| commit | 5e2bf8c82d08327044074330dff958fd32a8bcde (patch) | |
| tree | 49ba3a0c71c08e5b7f90694606fca5267662a4ad | |
| parent | 6de30e1985888a50b185ac72d4609fb41342bb8a (diff) | |
xmlprotocol: uncomment marshalling code for custom message
| -rw-r--r-- | ide/xmlprotocol.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index f1382fbcf..a4f133810 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -811,7 +811,7 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with let n, s = to_pair to_string to_string ns in WorkerStatus(n,s) | "goals", [loc;s] -> Goals (to_loc loc, to_string s) - (* | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x) *) + | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x) | "filedependency", [from; dep] -> FileDependency (to_option to_string from, to_string dep) | "fileloaded", [dirpath; filename] -> @@ -848,8 +848,8 @@ let of_feedback_content = function [of_pair of_string of_string (n,s)] | Goals (loc,s) -> constructor "feedback_content" "goals" [of_loc loc;of_string s] - (* | Custom (loc, name, x) -> *) - (* constructor "feedback_content" "custom" [of_loc loc; of_string name; x] *) + | Custom (loc, name, x) -> + constructor "feedback_content" "custom" [of_loc loc; of_string name; x] | FileDependency (from, depends_on) -> constructor "feedback_content" "filedependency" [ of_option of_string from; |