| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
|
This reverts commit ad2a0308b1592c7235714a2cca926f3b55accbb2.
|
|
|
|
buffer.
|
|
In particular, renouncing to original support for existing non .v
files in CoqIDE (hoping it is ok for anyone). Please amend if better
to propose.
|
|
|
|
|
|
Coqtop was wrongly assuming that receiving a SIGINT when reading on a channel
meant that the channel was closed, resulting in a crash when interrupting
an idle coqtop from CoqIDE.
To prevent this, we block SIGINTs when reading in ide_slave.
|
|
|
|
responsible about.
|
|
|
|
|
|
internal and external datatypes.
|
|
{Interface} instead.
|
|
- Extend the protocol with a new command called "annotate".
- By the way, relax the dependencies between the "ide" package
and the internal packages of Coq by *not* referring to external
type definitions inside Interface.
Indeed, the purpose of the protocol is to act as a barrier
between the source tree of Coq and the source tree of Coqide.
We should enforce this property.
(Maybe one day coqide will be extracted from the source tree
of Coq to live its own life.)
|
|
|
|
|
|
|
|
coqide to coqtop.
(Joint work with Pierre)
|
|
|
|
|
|
The leafs of the XML trees are still pretty-printed strings, but this
could be refined later on.
|
|
The more structured goal record type of CoqIDE is also useful for other
interfaces (in particular, for PIDE). To support this, the datatype was
factored out to the Proof module. In addition, the record gains a type
parameter, to allow interfaces to adapt the output to their needs.
To accommodate this type, the Proof module also gains the
map_structured_proof that takes a Proof.proof and a function on the
individual goals (in the context of an evar map) and produces a
structured goal based on the goal transformer.
|
|
|
|
|
|
|
|
|
|
This fix considerably speeds up syntax highlighting. It also avoids burning
100% CPU when typing long identifiers. Finally, identifiers longer than 20
characters are now properly highlighted, since the stack of the automaton
no longer overflows because of them.
|
|
See Eqdep_dec.v for instance. Module declarations were not highlighted
because the IDE wrongly believed they were used inside an unterminated
proof.
|
|
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
|
|
|
|
This way a user *can* use coqide with -debug
|
|
E.g.
Coq options are:
-I dir look for ML files in dir
-include dir (idem)
[...]
-h, --help print this list of options
With the flag '-toploop coqidetop' these extra option are also available:
--help-XML-protocol print the documentation of the XML protocol used by CoqIDE
|
|
Just like the [Record] keyword allows only non-recursive records.
|
|
|
|
|
|
This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses
don't respect Barendregt convention".
|
|
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
|
|
|
Sort of fixes bug #2765, but the file loading is broken and puts coqtop in
an inconsistent state, so that even the previous half-working patch was
actually not functionning at all. This should be fixed eventually.
|
|
died" when coqtop or coqtopide.cmxs are in inconsistent state.
|
|
|
|
|
|
reports errors also from stderr.
|
|
|
|
|
|
including bigger icons
|
|
|
