diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-02-11 02:13:30 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-05-31 09:38:57 +0200 |
commit | 91ee24b4a7843793a84950379277d92992ba1651 (patch) | |
tree | f176a54110e5f394acee26351c079a395dbf6a10 /lib/feedback.mli | |
parent | b994e3195d296e9d12c058127ced381976c3a49e (diff) |
Feedback cleanup
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
Diffstat (limited to 'lib/feedback.mli')
-rw-r--r-- | lib/feedback.mli | 81 |
1 files changed, 79 insertions, 2 deletions
diff --git a/lib/feedback.mli b/lib/feedback.mli index 0d8e20230..1e96f9a49 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -9,7 +9,7 @@ open Xml_datatype (* Old plain messages (used to be in Pp) *) -type message_level = +type level = | Debug of string | Info | Notice @@ -17,7 +17,7 @@ type message_level = | Error type message = { - message_level : message_level; + message_level : level; message_content : xml; } @@ -66,3 +66,80 @@ val of_feedback : feedback -> xml val to_feedback : xml -> feedback val is_feedback : xml -> bool +(** {6 Feedback sent, even asynchronously, to the user interface} *) + +(** Moved here from pp.ml *) + +(* Morally the parser gets a string and an edit_id, and gives back an AST. + * Feedbacks during the parsing phase are attached to this edit_id. + * The interpreter assignes an exec_id to the ast, and feedbacks happening + * during interpretation are attached to the exec_id. + * Only one among state_id and edit_id can be provided. *) + +(** A [logger] takes a level plus a pretty printing doc and logs it *) +type logger = level -> Pp.std_ppcmds -> unit + +(** [set_logger l] makes the [msg_*] to use [l] for logging *) +val set_logger : logger -> unit + +(** [std_logger] standard logger to [stdout/stderr] *) +val std_logger : logger + +val color_terminal_logger : logger +(* This logger will apply the proper {!Pp_style} tags, and in + particular use the formatters {!Pp_control.std_ft} and + {!Pp_control.err_ft} to display those messages. Be careful this is + not compatible with the Emacs mode! *) + +(** [feedback_logger] will produce feedback messages instead IO events *) +val feedback_logger : logger +val emacs_logger : logger + + +(** [set_feeder] A feeder processes the feedback, [ignore] by default *) +val set_feeder : (feedback -> unit) -> unit + +(** [feedback ?id ?route fb] produces feedback fb, with [route] and + [id] set appropiatedly, if absent, it will use the defaults set by + [set_id_for_feedback] *) +val feedback : + ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit + +(** [set_id_for_feedback route id] Set the defaults for feedback *) +val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit + +(** [with_output_to_file file f x] executes [f x] with logging + redirected to a file [file] *) +val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b + +(** {6 output functions} + +[msg_notice] do not put any decoration on output by default. If +possible don't mix it with goal output (prefer msg_info or +msg_warning) so that interfaces can dispatch outputs easily. Once all +interfaces use the xml-like protocol this constraint can be +relaxed. *) +(* Should we advertise these functions more? Should they be the ONLY + allowed way to output something? *) + +val msg_info : Pp.std_ppcmds -> unit +(** Message that displays information, usually in verbose mode, such as [Foobar + is defined] *) + +val msg_notice : Pp.std_ppcmds -> unit +(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *) + +val msg_warning : Pp.std_ppcmds -> unit +(** Message indicating that something went wrong, but without serious + consequences. *) + +val msg_error : Pp.std_ppcmds -> unit +(** Message indicating that something went really wrong, though still + recoverable; otherwise an exception would have been raised. *) + +val msg_debug : Pp.std_ppcmds -> unit +(** For debugging purposes *) + + + + |