| Age | Commit message (Collapse) | Author |
|---|
|
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|
|
|
|
|
|
We also move the Ltac-specific grammar to its folder.
|
|
|
|
Suggested by @ppedrot
|
|
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
|
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
|
|
|
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.
|
|
This has no influence on user-side, and only makes the life of the debugging
developer easier.
|
|
Instead of leaving the responsibility of extending the grammar to the caller,
we ask for a list of extensions in the return value of the function.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Once again showing the fragility of the parsing engine, commit a7917a32
reversed the relative order of the declaration of parsing rules for tactics
declared through TACTIC EXTEND. There is probably no good order at all, but
for retrocompatibility, this patch enforces the original one.
|
|
|
|
This reverts commit df1e24f64f68318221d08246098837368ee1b406.
|
|
subentry at a higher tactic level than the entry itself.
This is applicable to the parsing of expressions with infix or postfix
operators such as ; or ||.
Could be improved, e.g. so that no parenthesis are put when the
expression is the rightmost one, as in:
now (tac1;tac2)
where parentheses are not needed but still printed with this patch,
while the patch adds needed parentheses in
(now tac1);tac2
This would hardly scale to more complex grammars. E.g., if a suffix
expression can extend a leading expression as part of different
grammar entries, as in
let x := simpl in y ...
I don't see in general how to anticipate the need for parentheses
without restarting the parser to check the reversibility of the
printing.
|
|
|
|
|
|
|
|
|
|
Instead of relying on entry names as given by a hardwired registering
scheme in Pcoq, we recover them first through a user-defined map, and
fallback on generic argument names.
|
|
|
|
|
|
|
|
It was only used by setoid_ring for the Add Ring command, and was easily
replaced by a dedicated argument. Moreover, it was of no use to tactic
notations.
|
|
|
|
|
|
|
