diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-18 22:32:59 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-18 22:54:28 +0200 |
| commit | 411973d14a95b043f93ed6d0ca628a6a98e3c221 (patch) | |
| tree | ab5c9d7a2ce31bf17bfe2138ec7c98292ac15f0e /checker/print.ml | |
| parent | fa141fa1d2df2720f84a3e2c1fc4900a47f9939f (diff) | |
[checker] Fix/fine tune printing.
In 91ee24b4a7843793a84950379277d92992ba1651 , we discouraged direct
access to the console, recommending instead to provide information to
the user by means of the `Feedback.msg_*` facilities.
However, we introduced a display bug in the checker printer as it is
special and doesn't use the Pp facilities (likely for trust reasons),
spotted by @herbelin
This patch fixes this bug and performs a couple more of fine tunings in
the input.
However, it could be desirable to port the `checker/printer.ml` to `Pp`
and use the feedback mechanism; this would allow IDEs to use the checker
in a more convenient way, at the cost of trusting `Pp` (which is already
a bit trusted currently)
A start of that idea can be found at:
https://github.com/ejgallego/coq/tree/fix_checker_printing
Diffstat (limited to 'checker/print.ml')
| -rw-r--r-- | checker/print.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/checker/print.ml b/checker/print.ml index c0d1ac368..7ef752b00 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -10,7 +10,9 @@ open Format open Cic open Names -let print_instance i = Feedback.msg_notice (Univ.Instance.pr i) +let chk_pp = Pp.pp_with Format.std_formatter + +let print_instance i = chk_pp (Univ.Instance.pr i) let print_pure_constr csr = let rec term_display c = match c with @@ -108,7 +110,7 @@ let print_pure_constr csr = and sort_display = function | Prop(Pos) -> print_string "Set" | Prop(Null) -> print_string "Prop" - | Type u -> print_string "Type("; Feedback.msg_notice (Univ.pr_uni u); print_string ")" + | Type u -> print_string "Type("; chk_pp (Univ.pr_uni u); print_string ")" and name_display = function | Name id -> print_string (Id.to_string id) |