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/ide_slave.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/ide_slave.ml')
| -rw-r--r-- | ide/ide_slave.ml | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index ae3dcd94a9..7619c1452e 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -428,7 +428,7 @@ let print_ast id = (** Grouping all call handlers together + error handling *) -let eval_call xml_oc log c = +let eval_call log c = let interruptible f x = catch_break := true; Control.check_for_interrupt (); @@ -474,13 +474,6 @@ let print_xml = with e -> let e = CErrors.push e in Mutex.unlock m; iraise e -let slave_logger xml_oc ?loc level message = - (* convert the message into XML *) - let msg = hov 0 message in - let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in - let xml = Xmlprotocol.of_message level loc (Richpp.richpp_of_pp message) in - print_xml xml_oc xml - let slave_feeder xml_oc msg = let xml = Xmlprotocol.of_feedback msg in print_xml xml_oc xml @@ -500,8 +493,9 @@ let loop () = CThread.thread_friendly_read in_ch s ~off:0 ~len) in let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in - Feedback.set_logger (slave_logger xml_oc); + Feedback.set_logger Feedback.feedback_logger; Feedback.add_feeder (slave_feeder xml_oc); + let f_log str = Feedback.(feedback (Message(Notice, None, Richpp.richpp_of_pp str))) in (* We'll handle goal fetching and display in our own way *) Vernacentries.enable_goal_printing := false; Vernacentries.qed_display_script := false; @@ -511,7 +505,7 @@ let loop () = (* pr_with_pid (Xml_printer.to_string_fmt xml_query); *) let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in let () = pr_debug_call q in - let r = eval_call xml_oc (slave_logger xml_oc Feedback.Notice) q in + let r = eval_call f_log q in let () = pr_debug_answer q r in (* pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *) print_xml xml_oc (Xmlprotocol.of_answer q r); |