From e020cc70578b65609ac7337537f16a1c25254e77 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 31 May 2016 12:16:40 +0200 Subject: Move serialization functions out of Stm Serialization should be specific to each particular backend, so we let the Stm clients choose how the send the nodes. This should be quite safe to pull in. Test suite passes. Related to #180 --- ide/ide_slave.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'ide/ide_slave.ml') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 59efc2d821..4b043661e0 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -393,6 +393,15 @@ let interp ((_raw, verbose), s) = let quit = ref false +(** Serializes the output of Stm.get_ast *) +let print_ast id = + match Stm.get_ast id with + | Some (expr, loc) -> begin + try Texmacspp.tmpp expr loc + with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e) + end + | None -> Xml_datatype.PCData "ERROR" + (** Grouping all call handlers together + error handling *) let eval_call xml_oc log c = @@ -423,7 +432,7 @@ let eval_call xml_oc log c = Interface.interp = interruptible interp; Interface.handle_exn = handle_exn; Interface.stop_worker = Stm.stop_worker; - Interface.print_ast = Stm.print_ast; + Interface.print_ast = print_ast; Interface.annotate = interruptible annotate; } in Xmlprotocol.abstract_eval_call handler c -- cgit v1.2.3 From ffd89ea323937b7d323e24a2b6d53cdc857117dd Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 1 Jun 2016 16:51:15 +0200 Subject: Encapsulate xml serialization in xmlprotocol.mli This eases the task of replacing/improving the serializer, as well as making it more resistant. See pitfalls below: Main changes are: - fold `message` type into `feedback` type - make messages of type `Richpp.richpp` so we are explicit about the content being a rich document. - moved serialization functions for messages and stateid to `Xmlprotocol` - improved a couple of internal API points (`is_message`). Tested. --- ide/ide_slave.ml | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) (limited to 'ide/ide_slave.ml') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 4b043661e0..0e09d84095 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -453,16 +453,12 @@ let print_xml = let slave_logger xml_oc level message = (* convert the message into XML *) let msg = hov 0 message in - let message = { - Feedback.message_level = level; - Feedback.message_content = (Richpp.repr (Richpp.richpp_of_pp msg)); - } in - let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in - let xml = Feedback.of_message message in + let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in + let xml = Xmlprotocol.of_message level (Richpp.richpp_of_pp message) in print_xml xml_oc xml let slave_feeder xml_oc msg = - let xml = Feedback.of_feedback msg in + let xml = Xmlprotocol.of_feedback msg in print_xml xml_oc xml (** The main loop *) -- cgit v1.2.3