| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
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
|
| |
|
| |
|
|
|
|
| |
The created bundle contains only coqide and gtk (no coqtop, no stdlib)
|
| |
|
| |
|
|
|
|
| |
coqide --help.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
lib/interface split into:
- lib/feedback
subscribe-based feedback bus (also used by coqidetop)
- ide/interface
definition of coqide protocol messages
lib/pp
structured info/err/warn messages
lib/serialize split into:
- lib/serialize
generic xml serialization (list, pairs, int, loc, ...)
used by coqide but potentially useful to other interfaces
- ide/xmlprotocol
serialization of protocol messages as in ide/interface
the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
|
|
|
|
|
|
|
|
| |
The fix is only partial, because dropping files only works over the menu
bar, the icon bar, the status bar, and so on. Editable boxes, such as the
script widget, catch dnd events, hence preventing this code from working
for these drop targets. Some (labl)gtk expert should be able to sort it
out.
|
| |
|