| Age | Commit message (Collapse) | Author |
|---|
|
We mostly separate command line argument parsing from interpretation,
some (minor) imperative actions are still done at argument parsing
time. This tidies up the code quite a bit and allows to better follow
the complicated command line handling code.
To this effect, we group the key actions to be performed by the
toplevel into a new record type. There is still room to improve.
|
|
|
|
|
|
|
|
issue #6452
|
|
|
|
Should fix #6177, which was triggered by lonely .ml files.
|
|
This allows to focus on a sub-goal other than the first one without
resorting to the `Focus` command.
|
|
I don't understand what is wrong with putting a query in a script
running in the IDE. It is typically needed when giving demos, and that
sounds like a ligitimate use case. By the way, we do it ourselves every year
during the demo at CoqPL...
|
|
Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.
Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.
This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.
|
|
Extraction Language command
|
|
|
|
We move the main async flags to the STM in preparation for
more state encapsulation.
There is still more work to do, in particular we should make some of
the defaults a parameter instead of a flag.
|
|
|
|
|
|
I followed what seems to be the intention of the code, with the
original intention of remove the global imperative proof state.
However, I fully fail to see why the new API is better than the old
one. In fact the opposite seems the contrary.
Still big parts of the "new proof engine" seem unfinished, and I'm
afraid I am not the right person to know what direction things should
take.
|
|
Due to an API change in laglgtk, we need to update CoqIDE. We use a
makefile hack so it can compile with lablgtk < 2.8.16, another option
would be to require 2.8.16 as a minimal dependency.
We also refactor travis to test more lablgtk versions.
We also need to account for improved attribute handling in 4.06.0, in
particular module aliases will propagate the deprecation status.
Fixes #6140.
|
|
- Removing tag "found" (unused since bd18c0821 "Now CoqIDE has a nice
find & replace mechanism").
- Removing setting the priority of the debugging tag edit_zone: it was
set at exactly the level it would have been by default minus 1,
which is the level of tooltip, which have no associated visible
markers, so the setting was a priori w/o effect.
- For clarity, reorganizing order of tags into ephemere ones and non
ephemere ones.
|
|
We change the relative priority of errors and warnings, so that the
error takes precedence.
It is unsure that it is universally the best choice. If the location
of the error is finer than the one of the warning, it is better. In
the other way round, it might be less good, e.g. if understanding the
warning helps to understand the error.
Maybe the best policy would be to test the relative locations of the
warning and error?
Trying to consider the error as more important, at the current time.
|
|
Julien Narboux confirmed that it was dead code (GeoProof is not to be
confused with GeoCoq).
|
|
We make the Stm API functional over an opaque `doc` type. This allows
to have a much better picture of what the toplevel is doing; now
almost all users of STM private data are marked by typing.
For now only, the API is functional; a PR switching the internals
should come soon thou; however we must first fix some initialization
bugs.
Due to some users, we modify `feedback` internally to include a
"document id" field; we don't expose this change in the IDE protocol
yet.
|
|
See the discussion in the bug tracker, basically the STM delays the
feedback error message to a point where CoqIDE has forgotten about the
sentence, thus we were processing such errors in the generic case,
printing them twice as the Fail case will also do it.
We could indeed revert back to the 8.6 strategy for error (print
always from Fail and ignore Feedback), however I feel that time will
be better spent by fixing the STM than adding more CoqIDE workarounds.
|
|
|
|
|
|
|
|
This prevents seeing things like MsgDirectory which are actually
intended to be two distinct words.
|
|
|
|
|
|
We let the user choose the most appropriate action to do if coqtop decides
to go berserk.
|
|
Windows such as Search & Replace are dialogs. For some window
managers, the hint changes how the window is displayed.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This file doesn't want to leave us.
|
|
This fixes bug #5380 in particular.
More generally, tags were not updated to the correct default value
if the corresponding line in the configuration file was missing.
|
|
|
|
|
|
|
|
This is necessary in order for clients to identify the results of
queries. This is a minor breaking change of the protocol, affecting
only this particular call.
This change is necessary in order to fix bug ####.
|
|
Due to the situation explained in bug 5360, error printing in
ide_slave results in an anomaly. We fix that by properly processing
the error.
This fixes BZ#5524, however BZ#5525 , still applies.
|
|
|
|
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
|
|
|
There was a mistake in the conflict resolution of merge
6f2c19a1054ce58927dfa5b33131c3665fd5fdf8 which wrongly undid the the
deletion of the file `ide/texmacspp.ml` in 6a412da , fixing here and
sorry for the problem.
|
|
more uniform
|
