| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is the good parts of PR #360.
IIUC, these vernacular were meant mostly for debugging and they are
not supposed to be of any use these days.
Back and join are still there not to break the testing infrastructure,
but some day they should go away.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.
There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
explicitly asked so.
See discussion at PR #417 for more information.
|
| | |
| |
| |
| | |
RawLocal -> CLocal
|
| | |
| |
| |
| | |
This is a bit long, but it is to keep a symmetry with constr_expr.
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
For legacy reasons, pretty printing required to provide a "tag"
interpretation function `pp_tag`. However such function was not of much
use as the backends (richpp and terminal) hooked at the `Format.tag`
level.
We thus remove this unused indirection layer and annotate expressions
with their `Format` tags.
This is a step towards moving the last bit of terminal code out of the
core system.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
This is what has always been used, so it doesn't represent a functional
change.
This is just a preliminary patch, but many more possibilities could be
done wrt tags.
|
| | |
| |
| |
| | |
No functional change.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
Was a bug introduced in 0ad6edc1.
|
| |\| |
|
| | |
| |
| |
| |
| | |
We introduce a bit of compatibility parsing code to print deprecation
warnings.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing
changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341.
It turns out that calling from fake_ide the STM commands that were removed
by this PR requires an extension of the XML protocol. So postponing the
integration.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
I think these commands never make a lot of sense on scripts other than
debugging and we have better methods now.
The last remaining command, used for the tty emulation has been renamed
to VtBack, but it should go away at some point too once the legacy
interfaces are removed.
|
| | |\
| | |
| | |
| | | |
Was PR#339: Documenting type class options, typeclasses eauto
|
| | | |
| | |
| | |
| | | |
This was for the translator and is not relevant for the beautifier.
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#340: Fix various shortcomings of the warnings infrastructure.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
|
| | | |/
| |/|
| | |
| | |
| | | |
With multiple arguments list, repeating the "/" modifier used to be
mandatory. So instead of forbidding it, we issue a deprecation warning.
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- The flags are now interpreted from left to right, without any other
precedence rule. The previous one did not make much sense in interactive
mode.
- Set Warnings and Set Warnings Append are now synonyms, and have the
"append" semantics, which is the most natural one for warnings.
- Warnings on unknown warnings are now printed only once (previously the
would be repeated on further calls to Set Warnings, sections closing,
module requiring...).
- Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced
to "-foo" (if foo exists, "" otherwise).
|
| |\| |
|
| | |\
| | |
| | |
| | | |
Was PR#319: More error tagging, try to fix bug 5135
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#337: Fix arguments
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.
The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".
The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.
We also add *a lot* of missing checks on input values and fix various
bugs.
Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | | |
+ a few improvements on 5f1dd4c40 (lexing of { and }).
|
| | | | |
| | | |
| | | |
| | | | |
This is useful for debugging purposes.
|
| | | |/
| |/|
| | |
| | |
| | |
| | |
| | |
| | | |
The current tag system in `Pp` is generic, which implies we must choose
a tagging function when calling a printer.
For console printing there is a single choice, thus this commits adds it
a few missing cases.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | | |
This covers the case e.g. of "xₚ" (until the table of unicode
characters is upgraded!).
|
| | | |
| | |
| | |
| | |
| | | |
`Notation ".a" := nat.' was accepted and used for printing but not
recognized in parsing. Now it does. Other examples in test-suite.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The warning was pointless since the notation was accepted and parsed
anyway.
We now treat unrecognized unicode characters like ordinary
undefined tokens (e.g. "#" in a bare Coq).
For instance, "aₚ", or ".ₚ", or "?ₚ" now fail with "Undefined token"
rather than "Unsupported Unicode character".
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Given the current style in flags.mli no reason to have a function.
A deeper question is why a global flag is needed, in particular the use
in `interp/constrextern.ml` seems strange, the condition in the lexer
should be looked at and I'm not sure about `printing/`.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
8a8caba3).
- Adding cLexer.current_file to the lexer state, i.e. making it a
component of the type "coq_parsable" of lexer state (it was
forgotten in b8ae2de5 and 8a8caba3).
- Inlining save_translator/restore_translator which have now lost most
of their substance.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
It was not used any more by coqdoc since b8194b22 (Dec 2010).
The table is now only part of the lexer function closure
(and only in the camlp5 case).
|
| | |/ |
|
| |\| |
|
| | |
| |
| |
| |
| | |
done by the Ppcmd_comment token) and so that lexing/parsing
side-effects are collected at the same place, i.e. in CLexer.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
the state of parsable streams, so that different lexing/parsing
processes can be started independently without conflicting.
Note however that these different lexing/parsing processes cannot be
run concurrently as they still work on the same piece of global memory
(i.e. calls to entry_parse should remain atomic). To go further, one
would typically need to be able to functionally pass the lexing state
to each call to the lexer.
Note that currently the beautifier is also running in the context of a
lexer/parser state (for the mapping of location to comments).
In particular, this fixes #5102 (parsing/lexing of bullets depending on
the lexing state which was global).
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
We defactorize the in_clause grammar entry to allow parsing of the "symmetry"
tactic when it has no arguments. Beforehand, the clause_dft_concl entry
accepted the empty stream, preventing the definition of symmetry as a mere
identifier.
|
| | |
| |
| |
| |
| |
| |
| | |
This was introduced to implement the Append feature on options. As usual when
messing with predefined keywords, this broke code in the wild. In order not
to create a new keyword, we do the string analysis on the production branch of
parsing.
|
| |\| |
|
| | | |
|
Maxime Dénès
Emilio Jesus Gallego Arias
Hugo Herbelin
Pierre-Marie Pédrot
Ralf Jung
Guillaume Melquiond
Matthieu Sozeau