From 753b8f4aaa78fe1cf8ea033d8cf45e88b5da9d13 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 25 Jun 2014 17:04:35 +0200 Subject: all coqide specific files moved into ide/ lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/ --- ide/coq.ml | 56 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 28 insertions(+), 28 deletions(-) (limited to 'ide/coq.ml') diff --git a/ide/coq.ml b/ide/coq.ml index af00cc63c..c1555e57f 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -177,7 +177,7 @@ type void = Void Reference: http://alan.petitepomme.net/cwn/2004.01.13.html To rewrite someday with GADT. *) -type 'a poly_ccb = 'a Serialize.call * ('a Interface.value -> void) +type 'a poly_ccb = 'a Xmlprotocol.call * ('a Interface.value -> void) type 't scoped_ccb = { bind_ccb : 'a. 'a poly_ccb -> 't } type ccb = { open_ccb : 't. 't scoped_ccb -> 't } @@ -234,7 +234,7 @@ type coqtop = { (* called whenever coqtop dies *) mutable reset_handler : reset_kind -> unit task; (* called whenever coqtop sends a feedback message *) - mutable feedback_handler : Interface.feedback -> unit; + mutable feedback_handler : Feedback.feedback -> unit; (* actual coqtop process and its status *) mutable handle : handle; mutable status : status; @@ -296,22 +296,22 @@ let rec check_errors = function | `OUT :: _ -> raise (TubeError "OUT") let handle_intermediate_message handle xml = - let message = Serialize.to_message xml in - let level = message.Interface.message_level in - let content = message.Interface.message_content in + let message = Pp.to_message xml in + let level = message.Pp.message_level in + let content = message.Pp.message_content in let logger = match handle.waiting_for with | Some (_, l) -> l | None -> function - | Interface.Error -> Minilib.log ~level:`ERROR - | Interface.Info -> Minilib.log ~level:`INFO - | Interface.Notice -> Minilib.log ~level:`NOTICE - | Interface.Warning -> Minilib.log ~level:`WARNING - | Interface.Debug _ -> Minilib.log ~level:`DEBUG + | Pp.Error -> Minilib.log ~level:`ERROR + | Pp.Info -> Minilib.log ~level:`INFO + | Pp.Notice -> Minilib.log ~level:`NOTICE + | Pp.Warning -> Minilib.log ~level:`WARNING + | Pp.Debug _ -> Minilib.log ~level:`DEBUG in logger level content let handle_feedback feedback_processor xml = - let feedback = Serialize.to_feedback xml in + let feedback = Feedback.to_feedback xml in feedback_processor feedback let handle_final_answer handle xml = @@ -320,7 +320,7 @@ let handle_final_answer handle xml = | None -> raise (AnswerWithoutRequest (Xml_printer.to_string_fmt xml)) | Some (c, _) -> c in let () = handle.waiting_for <- None in - with_ccb ccb { bind_ccb = fun (c, f) -> f (Serialize.to_answer c xml) } + with_ccb ccb { bind_ccb = fun (c, f) -> f (Xmlprotocol.to_answer c xml) } type input_state = { mutable fragment : string; @@ -340,10 +340,10 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all = let l_end = Lexing.lexeme_end lex in state.fragment <- String.sub s l_end (String.length s - l_end); state.lexerror <- None; - if Serialize.is_message xml then begin + if Pp.is_message xml then begin handle_intermediate_message handle xml; loop () - end else if Serialize.is_feedback xml then begin + end else if Feedback.is_feedback xml then begin handle_feedback feedback_processor xml; loop () end else begin @@ -501,22 +501,22 @@ type 'a query = 'a Interface.value task let eval_call ?(logger=default_logger) call handle k = (** Send messages to coqtop and prepare the decoding of the answer *) - Minilib.log ("Start eval_call " ^ Serialize.pr_call call); + Minilib.log ("Start eval_call " ^ Xmlprotocol.pr_call call); assert (handle.alive && handle.waiting_for = None); handle.waiting_for <- Some (mk_ccb (call,k), logger); - Xml_printer.print handle.xml_oc (Serialize.of_call call); + Xml_printer.print handle.xml_oc (Xmlprotocol.of_call call); Minilib.log "End eval_call"; Void -let add ?(logger=default_logger) x = eval_call ~logger (Serialize.add x) -let edit_at i = eval_call (Serialize.edit_at i) -let query ?(logger=default_logger) x = eval_call ~logger (Serialize.query x) -let mkcases s = eval_call (Serialize.mkcases s) -let status ?logger force = eval_call ?logger (Serialize.status force) -let hints x = eval_call (Serialize.hints x) -let search flags = eval_call (Serialize.search flags) -let init x = eval_call (Serialize.init x) -let stop_worker x = eval_call (Serialize.stop_worker x) +let add ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.add x) +let edit_at i = eval_call (Xmlprotocol.edit_at i) +let query ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.query x) +let mkcases s = eval_call (Xmlprotocol.mkcases s) +let status ?logger force = eval_call ?logger (Xmlprotocol.status force) +let hints x = eval_call (Xmlprotocol.hints x) +let search flags = eval_call (Xmlprotocol.search flags) +let init x = eval_call (Xmlprotocol.init x) +let stop_worker x = eval_call (Xmlprotocol.stop_worker x) module PrintOpt = struct @@ -573,7 +573,7 @@ struct let mkopt o v acc = (o, Interface.BoolValue v) :: acc in let opts = Hashtbl.fold mkopt current_state [] in let opts = (width, Interface.IntValue !width_state) :: opts in - eval_call (Serialize.set_options opts) h + eval_call (Xmlprotocol.set_options opts) h (function | Interface.Good () -> k () | _ -> failwith "Cannot set options. Resetting coqtop") @@ -581,7 +581,7 @@ struct end let goals ?logger x h k = - PrintOpt.enforce h (fun () -> eval_call ?logger (Serialize.goals x) h k) + PrintOpt.enforce h (fun () -> eval_call ?logger (Xmlprotocol.goals x) h k) let evars x h k = - PrintOpt.enforce h (fun () -> eval_call (Serialize.evars x) h k) + PrintOpt.enforce h (fun () -> eval_call (Xmlprotocol.evars x) h k) -- cgit v1.2.3