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/interface.mli | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'ide/interface.mli') diff --git a/ide/interface.mli b/ide/interface.mli index 123cac6c22..43446f3918 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -12,15 +12,14 @@ type raw = bool type verbose = bool -type richpp = Richpp.richpp (** The type of coqtop goals *) type goal = { goal_id : string; (** Unique goal identifier *) - goal_hyp : richpp list; + goal_hyp : Pp.std_ppcmds list; (** List of hypotheses *) - goal_ccl : richpp; + goal_ccl : Pp.std_ppcmds; (** Goal conclusion *) } @@ -119,7 +118,7 @@ type edit_id = Feedback.edit_id should probably retract to that point *) type 'a value = | Good of 'a - | Fail of (state_id * location * richpp) + | Fail of (state_id * location * Pp.std_ppcmds) type ('a, 'b) union = ('a, 'b) Util.union @@ -203,7 +202,7 @@ type about_sty = unit type about_rty = coq_info type handle_exn_sty = Exninfo.iexn -type handle_exn_rty = state_id * location * richpp +type handle_exn_rty = state_id * location * Pp.std_ppcmds (* Retrocompatibility stuff *) type interp_sty = (raw * verbose) * string -- cgit v1.2.3 From aa9e94275ccac92311a6bdac563b61a6c7876cec Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 17 Mar 2017 20:27:44 +0100 Subject: [ide protocol] Add comment about leftover parameter. We try to address @silene 's concerns, which indeed are legitimate. --- ide/interface.mli | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'ide/interface.mli') diff --git a/ide/interface.mli b/ide/interface.mli index 43446f3918..9ed6062588 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -127,9 +127,13 @@ type ('a, 'b) union = ('a, 'b) Util.union (** [add ((s,eid),(sid,v))] adds the phrase [s] with edit id [eid] on top of the current edit position (that is asserted to be [sid]) verbosely if [v] is true. The response [(id,(rc,s)] is the new state - [id] assigned to the phrase, some output [s]. [rc] is [Inl] if the new + [id] assigned to the phrase. [rc] is [Inl] if the new state id is the tip of the edit point, or [Inr tip] if the new phrase - closes a focus and [tip] is the new edit tip *) + closes a focus and [tip] is the new edit tip + + [s] used to contain Coq's console output and has been deprecated + in favor of sending feedback, it will be removed in a future + version of the protocol. *) type add_sty = (string * edit_id) * (state_id * verbose) type add_rty = state_id * ((unit, state_id) union * string) @@ -142,8 +146,12 @@ type add_rty = state_id * ((unit, state_id) union * string) type edit_at_sty = state_id type edit_at_rty = (unit, state_id * (state_id * state_id)) union -(** [query s id] executes [s] at state [id] and does not record any state - change but for the printings that are sent in response *) +(** [query s id] executes [s] at state [id]. + + query used to reply with the contents of Coq's console output, and + has been deprecated in favor of sending the query answers as + feedback. It will be removed in a future version of the protocol. +*) type query_sty = string * state_id type query_rty = string -- cgit v1.2.3