| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
When one jumps from a focused area to a point after the focused zone,
sentences that are already processed (in the Doc.context of the focused
area) have not to be processed again (they are tagged as `Skip).
Detection of such sentences was based on tags (i.e. colors) that is shaky.
Now we use the sentence-marks as stored in the document data structure.
|
| | | |
| | |
| | |
| | | |
They used to be called output and output' ...
|
| | | |
| | |
| | |
| | | |
So that a module can add his own and look at the traffic
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | | |
Instead of relying on the current position of the cursor, we rather use
a dedicated mark in the message view.
|
| | | |
| | |
| | |
| | | |
in the Ocaml standard library
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
This allows a smoother transition between various versions of CoqIDE, by
not erasing options which are unknown at the present time.
|
| | | |
| | |
| | |
| | |
| | | |
The helper code in LablGTK is algorithmically slow, so that
we rather reimplement it as a small helper function.
|
| | | | |
|
| | | | |
|
| |/ / |
|
| | |
| |
| |
| | |
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.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
In Coqide 8.5pl2, "forward one command" (down arrow) always repositions the insertion point at the end of the phrase being executed, just after the final ".".
In Coqide 8.4, the insertion point is not moved if it is after the end of the executed phrase. The insertion point is moved only if it falls behind the phrase being executed.
I find the 8.5 behavior to be a regression over the lot more useful 8.4 behavior. This commit restores the 8.4 behavior of "forward one command".
|
| | |
| |
| |
| | |
Fixes both bugs #4924 and #4437.
|
| | |
| |
| |
| |
| |
| | |
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
|
| |\| |
|
| |\ \
| | |
| | |
| | | |
Was PR#223: Allow feedback messages to carry a location.
|
| | | |
| | |
| | |
| | | |
Cf CHANGES for details.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Instead of relaunching the coqtop process and then open the warning window,
we rather fire the warning and wait for the user to press the OK button before
doing anything.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The ErrorMsg datatype was introduced to allow locations in messages,
however, it was redundant with error and used only in one place.
We remove it in favor of a more uniform treatment of messages with
location. This patch also removes the use of `Loc.ghost` in one place.
Lightly tested.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
The new warnings mechanism may which to forward a location to
IDEs. This also makes sense for other message types.
Next step is to remove redundant MsgError feedback type.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/ /
| |
| |
| | |
IMO level indicators are not the proper place to store this information.
|
| | |
| |
| |
| |
| | |
Used to be an `exit 1`, now an error message is printed on stderr.
This helps people experimenting with the XML protocol.
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
This is the "error resiliency" mode for STM
|
| |\ \ \ \
| | |_|/
| |/| | |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The error message was not only causing coqtop to exit, but also coqide to
crash, which led to a rather poor user experience. Since the code does not
actually care about the file extension, this commit just removes the test.
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| | |_|_|/ /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
There is little point in telling the user the error report is sub optimal.
In this particular case, such error has already been reported (on
the correct location) so reminding it in a non-localized way is not
even that bad.
|
| | |_|_|/
|/| | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This makes the core free from particular protocol choices.
It should help with the ppx serialization project and shrinks clib.cma a
bit.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This eases the task of replacing/improving the serializer, as well as
making it more resistant. See pitfalls below:
Main changes are:
- fold `message` type into `feedback` type
- make messages of type `Richpp.richpp` so we are explicit about the
content being a rich document.
- moved serialization functions for messages and stateid to `Xmlprotocol`
- improved a couple of internal API points (`is_message`).
Tested.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Serialization should be specific to each particular backend, so we let
the Stm clients choose how the send the nodes.
This should be quite safe to pull in. Test suite passes.
Related to #180
|
Pierre-Marie Pédrot
Enrico Tassi
Matej Kosik
Matej Kosik
Emilio Jesus Gallego Arias
Xavier Leroy
Pierre Letouzey
Maxime Dénès
Daniel de Rauglaudre
Guillaume Melquiond