From f1c5e2ce2a4515a7c90c5ca22aa6eff22dd2f5ff Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 28 Jun 2016 16:52:46 +0200 Subject: [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. --- ide/xmlprotocol.ml | 6 ------ 1 file changed, 6 deletions(-) (limited to 'ide/xmlprotocol.ml') 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 -- cgit v1.2.3 From 5b8bfee9d80e550cd81e326ec134430b2a4797a5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Sep 2016 16:30:21 +0200 Subject: [pp] Make feedback the only logging mechanism. Previously to this patch, Coq featured to distinct logging paths: the console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format` module, and the `Feedback` one, intended to encapsulate message inside a more general, GUI-based feedback protocol. This patch removes the legacy logging path and makes feedback canonical. Thus, the core of Coq has no dependency on console code anymore. Additionally, this patch resolves the duplication of "document" formats present in the same situation. The original console-based printing code relied on an opaque datatype `std_ppcmds`, (mostly a reification of `Format`'s format strings) that could be then rendered to the console. However, the feedback path couldn't reuse this type due to its opaque nature. The first versions just embedded rending of `std_ppcmds` to a string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was introduced. The idea for this type was to be serializable, however it brought several problems: it didn't have proper document manipulation operations, its format was overly verbose and didn't preserve the full layout, and it still relied on `Format` for generation, making client-side rendering difficult. We thus follow the plan outlined in CEP#9, that is to say, we take a public and refactored version of `std_ppcmds` as the canonical "document type", and move feedback to be over there. The toplevel now is implemented as a feedback listener and has ownership of the console. `richpp` is now IDE-specific, and only used for legacy rendering. It could go away in future versions. `std_ppcmds` carries strictly more information and is friendlier to client-side rendering and display control. Thus, the new panorama is: - `Feedback` has become a very module for event dispatching. - `Pp` contains a target-independent box-based document format. It also contains the `Format`-based renderer. - All console access lives in `toplevel`, with console handlers private to coqtop. _NOTE_: After this patch, many printing parameters such as printing width or depth should be set client-side. This works better IMO, clients don't need to notify Coq about resizing anywmore. Indeed, for box-based capable backends such as HTML or LaTeX, the UI can directly render and let the engine perform the word breaking work. _NOTE_: Many messages could benefit from new features of the output format, however we have chosen not to alter them to preserve output. A Future commits will move console tag handling in `Pp_style` to `toplevel/`, where it logically belongs. The only change with regards to printing is that the "Error:" header was added to console output in several different positions, we have removed some of this duplication, now error messages should be a bit more consistent. --- ide/xmlprotocol.ml | 71 +++++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 57 insertions(+), 14 deletions(-) (limited to 'ide/xmlprotocol.ml') diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 65f44fdd38..08f23d3d4e 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -97,6 +97,49 @@ let to_richpp xml = match xml with | Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x | x -> raise Serialize.(Marshal_error("richpp",x)) +let of_box (ppb : Pp.block_type) = let open Pp in match ppb with + | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] + | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] + | Pp_hvbox i -> constructor "ppbox" "hvbox" [of_int i] + | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i] + +let to_box = let open Pp in + do_match "ppbox" (fun s args -> match s with + | "hbox" -> Pp_hbox (to_int (singleton args)) + | "vbox" -> Pp_vbox (to_int (singleton args)) + | "hvbox" -> Pp_hvbox (to_int (singleton args)) + | "hovbox" -> Pp_hovbox (to_int (singleton args)) + | x -> raise (Marshal_error("*ppbox",PCData x)) + ) + +let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with + | Ppcmd_empty -> constructor "ppdoc" "emtpy" [] + | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] + | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] + | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)] + | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair (of_list of_string) of_pp (t,s)] + | Ppcmd_print_break (i,j) + -> constructor "ppdoc" "break" [of_pair of_int of_int (i,j)] + | Ppcmd_force_newline -> constructor "ppdoc" "newline" [] + | Ppcmd_comment cmd -> constructor "ppdoc" "comment" [of_list of_string cmd] + + +let rec to_pp xpp = let open Pp in + do_match "ppdoc" (fun s args -> match s with + | "empty" -> Ppcmd_empty + | "string" -> Ppcmd_string (to_string (singleton args)) + | "glue" -> Ppcmd_glue (to_list to_pp (singleton args)) + | "box" -> let (bt,s) = to_pair to_box to_pp (singleton args) in + Ppcmd_box(bt,s) + | "tag" -> let (tg,s) = to_pair (to_list to_string) to_pp (singleton args) in + Ppcmd_tag(tg,s) + | "break" -> let (i,j) = to_pair to_int to_int (singleton args) in + Ppcmd_print_break(i, j) + | "newline" -> Ppcmd_force_newline + | "comment" -> Ppcmd_comment (to_list to_string (singleton args)) + | x -> raise (Marshal_error("*ppdoc",PCData x)) + ) xpp + let of_value f = function | Good x -> Element ("value", ["val", "good"], [f x]) | Fail (id,loc, msg) -> @@ -104,7 +147,7 @@ let of_value f = function | None -> [] | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in let id = of_stateid id in - Element ("value", ["val", "fail"] @ loc, [id; of_richpp msg]) + Element ("value", ["val", "fail"] @ loc, [id; of_pp msg]) let to_value f = function | Element ("value", attrs, l) -> @@ -120,7 +163,7 @@ let to_value f = function in let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in let id = to_stateid id in - let msg = to_richpp msg in + let msg = to_pp msg in Fail (id, loc, msg) else raise (Marshal_error("good or fail",PCData ans)) | x -> raise (Marshal_error("value",x)) @@ -147,15 +190,15 @@ let to_evar = function | x -> raise (Marshal_error("evar",x)) let of_goal g = - let hyp = of_list of_richpp g.goal_hyp in - let ccl = of_richpp g.goal_ccl in + let hyp = of_list of_pp g.goal_hyp in + let ccl = of_pp g.goal_ccl in let id = of_string g.goal_id in Element ("goal", [], [id; hyp; ccl]) let to_goal = function | Element ("goal", [], [id; hyp; ccl]) -> - let hyp = to_list to_richpp hyp in - let ccl = to_richpp ccl in - let id = to_string id in + let hyp = to_list to_pp hyp in + let ccl = to_pp ccl in + let id = to_string id in { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } | x -> raise (Marshal_error("goal",x)) @@ -344,8 +387,8 @@ end = struct Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals else let pr_goal { goal_hyp = hyps; goal_ccl = goal } = - "[" ^ String.concat "; " (List.map Richpp.raw_print hyps) ^ " |- " ^ - Richpp.raw_print goal ^ "]" in + "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^ + Pp.string_of_ppcmds goal ^ "]" in String.concat " " (List.map pr_goal g.fg_goals) let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]" let pr_status (s : status) = @@ -701,10 +744,10 @@ let to_call : xml -> unknown_call = let pr_value_gen pr = function | Good v -> "GOOD " ^ pr v - | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^Richpp.raw_print str^"]" + | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^ Pp.string_of_ppcmds str ^ "]" | Fail (id,Some(i,j),str) -> "FAIL "^Stateid.to_string id^ - " ("^string_of_int i^","^string_of_int j^")["^Richpp.raw_print str^"]" + " ("^string_of_int i^","^string_of_int j^")["^Pp.string_of_ppcmds str^"]" let pr_value v = pr_value_gen (fun _ -> "FIXME") v let pr_full_value : type a. a call -> a value -> string = fun call value -> match call with | Add _ -> pr_value_gen (print add_rty_t ) value @@ -760,7 +803,7 @@ let document to_string_fmt = (to_string_fmt (of_value (fun _ -> PCData "b") (Good ()))); Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n" (to_string_fmt (of_value (fun _ -> PCData "b") - (Fail (Stateid.initial,Some (15,34),Richpp.richpp_of_string "error message")))); + (Fail (Stateid.initial,Some (15,34), Pp.str "error message")))); document_type_encoding to_string_fmt (* Moved from feedback.mli : This is IDE specific and we don't want to @@ -787,12 +830,12 @@ let to_message_level = let of_message lvl loc msg = let lvl = of_message_level lvl in let xloc = of_option of_loc loc in - let content = of_richpp msg in + let content = of_pp msg in Xml_datatype.Element ("message", [], [lvl; xloc; content]) let to_message xml = match xml with | Xml_datatype.Element ("message", [], [lvl; xloc; content]) -> - Message(to_message_level lvl, to_option to_loc xloc, to_richpp content) + Message(to_message_level lvl, to_option to_loc xloc, to_pp content) | x -> raise (Marshal_error("message",x)) let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with -- cgit v1.2.3 From 4084ee30293a6013592c0651dfeb1975711f135f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 30 Nov 2016 22:24:17 +0100 Subject: [ide] richpp clenaup We remove the "abstraction breaking" primitives and reduce the file to the used fragment. --- ide/xmlprotocol.ml | 5 ----- 1 file changed, 5 deletions(-) (limited to 'ide/xmlprotocol.ml') diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 08f23d3d4e..6ed62082d7 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -92,11 +92,6 @@ let to_stateid = function let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)],[]) -let of_richpp x = Element ("richpp", [], [Richpp.repr x]) -let to_richpp xml = match xml with - | Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x - | x -> raise Serialize.(Marshal_error("richpp",x)) - let of_box (ppb : Pp.block_type) = let open Pp in match ppb with | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] -- cgit v1.2.3 From a8ec2dc5c330ded1ba400ef202c57e68d2533312 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 5 Dec 2016 18:17:46 +0100 Subject: [pp] Remove special tag type and handler from Pp. For legacy reasons, pretty printing required to provide a "tag" interpretation function `pp_tag`. However such function was not of much use as the backends (richpp and terminal) hooked at the `Format.tag` level. We thus remove this unused indirection layer and annotate expressions with their `Format` tags. This is a step towards moving the last bit of terminal code out of the core system. --- ide/xmlprotocol.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ide/xmlprotocol.ml') diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 6ed62082d7..1d50aed032 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -112,7 +112,7 @@ let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)] - | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair (of_list of_string) of_pp (t,s)] + | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair of_string of_pp (t,s)] | Ppcmd_print_break (i,j) -> constructor "ppdoc" "break" [of_pair of_int of_int (i,j)] | Ppcmd_force_newline -> constructor "ppdoc" "newline" [] @@ -126,7 +126,7 @@ let rec to_pp xpp = let open Pp in | "glue" -> Ppcmd_glue (to_list to_pp (singleton args)) | "box" -> let (bt,s) = to_pair to_box to_pp (singleton args) in Ppcmd_box(bt,s) - | "tag" -> let (tg,s) = to_pair (to_list to_string) to_pp (singleton args) in + | "tag" -> let (tg,s) = to_pair to_string to_pp (singleton args) in Ppcmd_tag(tg,s) | "break" -> let (i,j) = to_pair to_int to_int (singleton args) in Ppcmd_print_break(i, j) -- cgit v1.2.3 From 829a8feb3d02da057d39b5029b422e8a45dd1608 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 25 Jan 2017 14:39:29 +0100 Subject: [xml] Restore protocol compatibility with 8.6. By default, we serialize messages to the "rich printing representation" as it was done in 8.6, this ways clients don't have to adapt unless they specifically request the new format using option `--xml_format=Ppcmds` --- ide/xmlprotocol.ml | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'ide/xmlprotocol.ml') diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 1d50aed032..b4f2ad0bef 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -12,6 +12,9 @@ let protocol_version = "20150913" +type msg_format = Richpp of int | Ppcmds +let msg_format = ref (Richpp 72) + (** * Interface of calls to Coq by CoqIde *) open Util @@ -135,6 +138,14 @@ let rec to_pp xpp = let open Pp in | x -> raise (Marshal_error("*ppdoc",PCData x)) ) xpp +let of_richpp x = Element ("richpp", [], [x]) + +(* Run-time Selectable *) +let of_pp (pp : Pp.std_ppcmds) = + match !msg_format with + | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp) + | Ppcmds -> of_pp pp + let of_value f = function | Good x -> Element ("value", ["val", "good"], [f x]) | Fail (id,loc, msg) -> @@ -669,6 +680,9 @@ let of_answer : type a. a call -> a value -> xml = function | PrintAst _ -> of_value (of_value_type print_ast_rty_t ) | Annotate _ -> of_value (of_value_type annotate_rty_t ) +let of_answer msg_fmt = + msg_format := msg_fmt; of_answer + let to_answer : type a. a call -> xml -> a value = function | Add _ -> to_value (to_value_type add_rty_t ) | Edit_at _ -> to_value (to_value_type edit_at_rty_t ) @@ -902,6 +916,9 @@ let of_feedback msg = let route = string_of_int msg.route in Element ("feedback", obj @ ["route",route], [id;content]) +let of_feedback msg_fmt = + msg_format := msg_fmt; of_feedback + let to_feedback xml = match xml with | Element ("feedback", ["object","edit";"route",route], [id;content]) -> { id = Edit(to_edit_id id); -- cgit v1.2.3 From fb04bc5cae0d648c379b9eb44f8b515f8e15b854 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 17 Mar 2017 18:12:03 +0100 Subject: [pp] Hide the internal representation of `std_ppcmds`. Following a suggestion by @ppedrot in #390, we require `Pp` clients to be aware that they are using a "view" on the `std_ppcmds` type. This is not extremely useful as people caring about the documents will indeed have to follow changes in the view, but it costs little to play on the safe side here for now. We also introduce a more standard notation, `Pp.t` for the main type. --- ide/xmlprotocol.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'ide/xmlprotocol.ml') diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index b4f2ad0bef..5f80d68974 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -110,7 +110,7 @@ let to_box = let open Pp in | x -> raise (Marshal_error("*ppbox",PCData x)) ) -let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with +let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with | Ppcmd_empty -> constructor "ppdoc" "emtpy" [] | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] @@ -123,6 +123,7 @@ let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with let rec to_pp xpp = let open Pp in + Pp.unrepr @@ do_match "ppdoc" (fun s args -> match s with | "empty" -> Ppcmd_empty | "string" -> Ppcmd_string (to_string (singleton args)) -- cgit v1.2.3