| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
-> Candidate to be merge with the main feedback commit.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Previously to this patch, Coq featured to distinct logging paths: the
console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format`
module, and the `Feedback` one, intended to encapsulate message inside a
more general, GUI-based feedback protocol.
This patch removes the legacy logging path and makes feedback
canonical. Thus, the core of Coq has no dependency on console code
anymore.
Additionally, this patch resolves the duplication of "document" formats
present in the same situation. The original console-based printing code
relied on an opaque datatype `std_ppcmds`, (mostly a reification of
`Format`'s format strings) that could be then rendered to the console.
However, the feedback path couldn't reuse this type due to its opaque
nature. The first versions just embedded rending of `std_ppcmds` to a
string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was
introduced.
The idea for this type was to be serializable, however it brought
several problems: it didn't have proper document manipulation
operations, its format was overly verbose and didn't preserve the full
layout, and it still relied on `Format` for generation, making
client-side rendering difficult.
We thus follow the plan outlined in CEP#9, that is to say, we take a
public and refactored version of `std_ppcmds` as the canonical "document
type", and move feedback to be over there. The toplevel now is
implemented as a feedback listener and has ownership of the console.
`richpp` is now IDE-specific, and only used for legacy rendering. It
could go away in future versions. `std_ppcmds` carries strictly more
information and is friendlier to client-side rendering and display
control.
Thus, the new panorama is:
- `Feedback` has become a very module for event dispatching.
- `Pp` contains a target-independent box-based document format.
It also contains the `Format`-based renderer.
- All console access lives in `toplevel`, with console handlers private
to coqtop.
_NOTE_: After this patch, many printing parameters such as printing
width or depth should be set client-side. This works better IMO,
clients don't need to notify Coq about resizing anywmore. Indeed, for
box-based capable backends such as HTML or LaTeX, the UI can directly
render and let the engine perform the word breaking work.
_NOTE_: Many messages could benefit from new features of the output
format, however we have chosen not to alter them to preserve output.
A Future commits will move console tag handling in `Pp_style` to
`toplevel/`, where it logically belongs.
The only change with regards to printing is that the "Error:" header was
added to console output in several different positions, we have removed
some of this duplication, now error messages should be a bit more
consistent.
|
| |
|
|
|
|
|
|
|
|
|
| |
This reverts 4444768d3f4f9c4fcdd440f7ab902886bd8e2b09
(the mllib dependencies that should be surely tweaked more).
The logic for `fatal_error` has no place in `CErrors`, this is
coqtop-specific code.
What is more, a libobject caller should handle the exception correctly,
I fail to see why the fix was needed on the first place.
|
| | |
|
| | |
|
| |
|
|
| |
We replace open/close box commands in favor of the create box ones.
|
| |
|
|
| |
We replace open/close tag commands by a well-balanced "tag" wrapper.
|
| | |
|
| | |
|
| |
|
|
|
| |
We also remove flushing operations `msg_with`, now the flushing
responsibility belong to the owner of the formatter.
|
| |
|
|
| |
Mostly unused, we ought to limit spacing in the boxes themselves.
|
| |
|
|
|
|
|
|
| |
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.js
|
| | |
| |
| |
| | |
No functional change.
|
| | |
| |
| |
| | |
No functional changes.
|
| |/
|
|
| |
It was always set to `greedy:true`.
|
| |\ |
|
| | | |
|
| | | |
|
| |\ \ |
|
| |\ \ \ |
|
| | | |\ \ |
|
| |\ \ \ \ \
| | |/ / /
| |/| | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
The same file name for .dot graphs could be used by concurrent processes.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Coq expects aux_file_name_for to give the aux file corresponding to the
input file whichever its Coq-related extension, be it .v or .vo or .vio.
Commit 3e6fa1c broke this contract when fixing bug #5183. As a
consequence, depending on the execution path, Coq would try to save or
load from either .foo.aux or .foo.vo.aux or .foo.vio.aux.
This commit reverts 3e6fa1c and fixes bug #5183 much earlier in the call
chain by not initializing hints when the input file does not end with .v.
This also restores 8.5 behavior with respect to aux file naming.
|
| | | | | | |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#351: Complete a truncated comment
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
Was PR#363: lib/Unicodetable: Update.
|
| | | | | |/ /
| | | |/| |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Richpp output depends on printing width, thus its internal formatter
should be seeded with the proper width value.
While we are at it, we increase the default buffer size to a more
sensible value.
|
| |\ \ \ \ \ \
| | |_|/ / /
| |/| | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
When opening a file without extension, an uncaught exception was
occurring.
Note that this fix is not complete, since the "Compile Buffer" command
still fails. This is because of a limitation of coqc which appends the
".v" extension to its argument even if it already existed (and even if
it doesn't exist with the extension!).
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Note: "dependant" does exist, but it is a noun and it means a person that
is somehow financially dependent on someone else.
|
| |\| | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Unicode tables using UUCD, an OCaml library to parse the official
Unicode tables.
|
| | | | | | | |
|
| | |_|_|/ /
|/| | | | |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | | |
Introduce by myself, I'm afraid, in #308. Noticed by PMP during the
review, but I forgot to fix it before merge.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This made the whole pp code complicated only for the purpose of the
beautifier, while it is not clear when this was useful.
Removing the code for simplicity, not excluding to later address
beautifier issues when they show up.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We simply remove the warnings about paths mixing Win32 and Unix
separators, since that situation does not seem problematic (c.f.
discussion on the bug tracker).
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This was not detected by running coq-contribs, so it probably means that
we are not testing with the right version of OCaml.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- 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
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
It used to be Stateid.initial by default. That is indeed a valid
state id but very likely not the very best one (that would be
the tip of the document).
|
| |\| | | | |
|
| | | | | | |
|
| | |/ / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
In order to get proper coloring, we must tag the headers of error
messages in `CError`.
This should fix bug
https://coq.inria.fr/bugs/show_bug.cgi?id=5135
However, note that this could interact badly with the richpp printing
used by the IDE. At this level, we have no clue which tag we'd like to
apply, as we know (and shouldn't) nothing about the top level backend.
Thus, for now I've selected the console printer, hoping that the
`Richpp` won't crash the IDE.
|
| |\| | | |
|
Emilio Jesus Gallego Arias
Maxime Dénès
Pierre-Marie Pédrot
Guillaume Melquiond
Yann Régis-Gianas
CJ Bell
Arnaud Spiwack
Hugo Herbelin
Enrico Tassi