| Age | Commit message (Collapse) | Author |
|---|
|
internal and external datatypes.
|
|
- 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.)
|
|
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.
|
|
|
|
|
|
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/
|
