diff options
| author | Maxime Dénès | 2017-10-09 16:44:02 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-09 16:44:02 +0200 |
| commit | 1aeb43a3c7779001b0404d9dcc1603bf4c49dee0 (patch) | |
| tree | eea4ffe8d6a2e60ae134efab678e5a878a303097 /ide/xmlprotocol.ml | |
| parent | 5ef85c86dc94338c2d0da060946baafea2e5370e (diff) | |
| parent | 75c0c5c2b460614fba6705c6e0d64859815a613c (diff) | |
Merge PR #1087: [stm] Switch to a functional API
Diffstat (limited to 'ide/xmlprotocol.ml')
| -rw-r--r-- | ide/xmlprotocol.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index b452b0a13f..aaa24a2a95 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -939,7 +939,7 @@ let of_edit_or_state_id id = ["object","state"], of_stateid id let of_feedback msg = let content = of_feedback_content msg.contents in - let obj, id = of_edit_or_state_id msg.id in + let obj, id = of_edit_or_state_id msg.span_id in let route = string_of_int msg.route in Element ("feedback", obj @ ["route",route], [id;content]) @@ -947,8 +947,9 @@ let of_feedback msg_fmt = msg_format := msg_fmt; of_feedback let to_feedback xml = match xml with - | Element ("feedback", ["object","state";"route",route], [id;content]) -> { - id = to_stateid id; + | Element ("feedback", ["object","state";"route",route], [id;content]) -> { + doc_id = 0; + span_id = to_stateid id; route = int_of_string route; contents = to_feedback_content content } | x -> raise (Marshal_error("feedback",x)) |