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.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'ide/xmlprotocol.mli') diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index 1bb9989704..ca911178f5 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -66,7 +66,5 @@ val of_feedback : Feedback.feedback -> xml val to_feedback : xml -> Feedback.feedback val is_feedback : xml -> bool -val is_message : xml -> (Feedback.level * Loc.t option * Richpp.richpp) option val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml -(* val to_message : xml -> Feedback.message *) -- 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.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'ide/xmlprotocol.mli') diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index ca911178f5..f6fae24d7c 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -66,5 +66,6 @@ val of_feedback : Feedback.feedback -> xml val to_feedback : xml -> Feedback.feedback val is_feedback : xml -> bool -val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml +val of_message : Feedback.level -> Loc.t option -> Pp.std_ppcmds -> xml +(* val to_message : xml -> Feedback.message *) -- 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.mli | 4 ---- 1 file changed, 4 deletions(-) (limited to 'ide/xmlprotocol.mli') diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index f6fae24d7c..43a65dfa85 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -57,10 +57,6 @@ val pr_call : 'a call -> string val pr_value : 'a value -> string val pr_full_value : 'a call -> 'a value -> string -(** * Serialization of rich documents *) -val of_richpp : Richpp.richpp -> Xml_datatype.xml -val to_richpp : Xml_datatype.xml -> Richpp.richpp - (** * Serializaiton of feedback *) val of_feedback : Feedback.feedback -> xml val to_feedback : xml -> Feedback.feedback -- 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.mli | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'ide/xmlprotocol.mli') diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index 43a65dfa85..9cefab517f 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -40,12 +40,17 @@ val abstract_eval_call : handler -> 'a call -> 'a value val protocol_version : string +(** By default, we still output messages in Richpp so we are + compatible with 8.6, however, 8.7 aware clients will want to + set this to Ppcmds *) +type msg_format = Richpp of int | Ppcmds + (** * XML data marshalling *) val of_call : 'a call -> xml val to_call : xml -> unknown_call -val of_answer : 'a call -> 'a value -> xml +val of_answer : msg_format -> 'a call -> 'a value -> xml val to_answer : 'a call -> xml -> 'a value (* Prints the documentation of this module *) @@ -58,10 +63,7 @@ val pr_value : 'a value -> string val pr_full_value : 'a call -> 'a value -> string (** * Serializaiton of feedback *) -val of_feedback : Feedback.feedback -> xml +val of_feedback : msg_format -> Feedback.feedback -> xml val to_feedback : xml -> Feedback.feedback -val is_feedback : xml -> bool - -val of_message : Feedback.level -> Loc.t option -> Pp.std_ppcmds -> xml -(* val to_message : xml -> Feedback.message *) +val is_feedback : xml -> bool -- cgit v1.2.3