diff options
| author | Emilio Jesus Gallego Arias | 2016-06-28 16:52:46 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-21 15:47:13 +0100 |
| commit | f1c5e2ce2a4515a7c90c5ca22aa6eff22dd2f5ff (patch) | |
| tree | 2a295b6855f0bab21922ea8621ee3ce680e5e7dd /ide/xmlprotocol.ml | |
| parent | 28d3bb3c8bddc63d038d8d55a34c928675fa9f7b (diff) | |
[ide] Use "log via feedback".
We remove the custom logger handler in ide_slave, and handle everything
via feedback. This is an experimental patch but it seems to bring quite
a bit of cleanup and a more uniform handling to messaging.
Diffstat (limited to 'ide/xmlprotocol.ml')
| -rw-r--r-- | ide/xmlprotocol.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 5f82a8898b..65f44fdd38 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -795,12 +795,6 @@ let to_message xml = match xml with Message(to_message_level lvl, to_option to_loc xloc, to_richpp content) | x -> raise (Marshal_error("message",x)) -let is_message xml = - try begin match to_message xml with - | Message(l,c,m) -> Some (l,c,m) - | _ -> None - end with | Marshal_error _ -> None - let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "addedaxiom", _ -> AddedAxiom | "processed", _ -> Processed |