| Age | Commit message (Collapse) | Author |
|---|
|
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
|
Types were a bit difficult to read as they were mostly based on
anonymous products, this commit replaces them by named records and
refactors out some imperative code.
There is still quite a bit of room for improvement, but at least the
records provide a basis for more fine-grained understanding and
documentation.
|
|
|
|
|
|
Also getting rid of a global side-effect.
|
|
|
|
|
|
This is a quick fix. The Metasyntax module should be thoroughly revised
in trunk, because it starts featuring a lot of spaghetti code and redundant
data.
|
|
We also move the Ltac-specific grammar to its folder.
|
|
Suggested by @ppedrot
|
|
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
|
|
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 is a first step to relay location info in an uniform way, as needed
by warnings and other mechanisms.
The location info remains unused for now, but coqtop printing could take
advantage of it if so wished.
|
|
|
|
|
|
non-recursive notations (#4815).
|
|
|
|
|
|
This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e.
|
|
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.
|
|
|
|
|
|
|
|
|
|
When a notation was starting or ending a space, Coq assumed the notation
had no terminal symbol in either places. Coq also considered a notation
containing only spaces to be productive. As stated in the documentation,
extraneous spaces are only meant as printing hints, they are not meant to
have any influence on parsing.
|
|
This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
|
|
Notation "## c" := (S c) (at level 0, c at level 100).
which break the stratification of precedences. This works for the case
of infix or suffix operators which occur in only one grammar rule,
such as +, *, etc. This solves the "constr" part of #3709, even though
this example is artificial.
The fix is not complete. It puts extra parenthesese even when it is
end of sentence, as in
Notation "# c % d" := (c+d) (at level 3).
Check fun x => # ## x % ## (x * 2).
(* fun x : nat => # ## x % (## x * 2) *)
The fix could be improved by not always using 100 for the printing
level of "## c", but 100 only when not the end of the sentence.
The fix does not solve the general problem with symbols occurring in
more than one rule, as e.g. in:
Notation "# c % d" := (c+d) (at level 1).
Notation "## c" := (S c) (at level 0, c at level 5).
Check fun x => # ## x % 0.
(* Parentheses are necessary only if "0 % 0" is also parsable *)
I don't see in this case what better approach to follow than
restarting the parser to check reversibility of the printing.
|
|
could be used with arguments which are binding variables, as was done
in ssrfun.v.
|
|
|
|
|
|
|
|
- Making a clear distinction between expressions of the notation which
are associated to binding variables only (as in `Notation "'lam' x ,
P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2
(fun x:t => p) (fun x:t => q))') and those which are associated to
at list one subterm (e.g. `Notation "x .+1" := (S x)' but also
"Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))'
as in #4592). The former have type NtnTypeOnlyBinder.
- Thus avoiding in particular encoding too early Anonymous as GHole
and "Name id" as "GVar id".
There is a non-trivial alpha-conversion work to do to get #4592
working. See comments in Notation_ops.add_env.
|
|
|
|
|
|
We simply handle the "break" in error messages. Not sure it is the
proper bugfix though, we may want to be able to add breaks in such
recursive notations.
|
|
|
|
|
|
|
|
|
|
Actually the identifier was never used and just carried along.
|
|
The TacAlias node now only contains the arguments fed to the tactic notation.
The binding variables are worn by the tactic representation in Tacenv.
|
|
This commit has deep consequences in term of tactic evaluation,
as it allows to pass any tac_arg to ML and alias tactics rather than
mere generic arguments. This makes the evaluation much more uniform,
and in particular it removes the special evaluation function for notations.
This last point may break some notations out there unluckily.
I had to treat in an ad-hoc way the tactic(...) entry of tactic notations
because it is actually not interpreted as a generic argument but rather
as a proper tactic expression instead.
There is for now no syntax to pass any tactic argument to a given ML or
notation tactic, but this should come soon.
Also fixes bug #3849 en passant.
|
|
|
|
|
|
|
|
|
|
|
