| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
| |
For now, the only meaningful user is "Set Warnings". Example:
Section Bar.
Local Set Warnings Append "-foo".
(* warning foo is now disabled *)
End Bar.
(* foo is now reenabled, assuming it was before entering the section *)
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
When inserting a character in an already processed buffer, a message is
sent to Coq so that the proof is backtracked and the character is
inserted. If a second character is inserted while Coq is still busy with
the first message, the action is canceled, but the signal is no longer
dropped so that the second character is properly inserted.
|
| | |
| |
| | |
CoqIDE does not have a "display" menu. It has a "view" menu with a list of display options.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
This brings a 10x speedup for going at the end of large .v files.
|
| | | | |
| | | |
| | | |
| | | | |
This brings a 10x speedup for going at the end of large .v files.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This appends the currently selected word to the query. Only queries
that end with this are supported, "..." inside the query will just
not work.
|
| | | | | |
|
Guillaume Melquiond
Maxime Dénès
Pierre-Marie Pédrot
Théo Zimmermann
Enrico Tassi
Xavier Leroy
Pierre Letouzey
Daniel de Rauglaudre
Emilio Jesus Gallego Arias
Lionel Rieg
Cyprien Mangin