| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Current coq trunk has a bug with Show that I reported (there is a
spurious Show executed) which makes C-u C-c C-a C-s fail for now.
Should be fixed shortly.
|
|
|
|
This fixes a bunch of compilation warnings
|
|
[WIP] ELPA/MELPA support
|
|
|
|
This commit contributes to shorten the real time of Travis' automated build.
|
|
Closes ProofGeneral/PG#177
|
|
|
|
The code uses several token searcher and the wrong one was called
somewhere.
|
|
This change is intended as an intermediate step toward the removal
of the bundled copy of `mmm' package. Even with this change, PG
continues to use the bundled version, unless `mmm-auto' is already
loaded at the time PG first loads `proof-auxmodes'.
The benefit of this change is that tools that extract the features
provided and required by a package, such as those used to maintain
the Emacsmirror, will no longer be tricked into believing that
`mmm' is part of PG.
Eventually the bundled `mmm' copy should be removed completely, as I
suggested in #171, and as was already on the roadmap before I did so.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This file is `require'-d when compiling coq.el, and at that point the proof
assistant isn't set to coq yet, so it would define variables prefixed by `nil-'
instead of `coq'.
|
|
This file is `require'-d from other places, at compile time. This doesn't work
nicely with compilation by package.el (PG complains and says "defpacustom: Proof
assistant setting compile-before-require re-defined!")
|
|
The problem is that loading pg-custom runs a bunch of defpgcustom, with no
current proof assistant. Then when coq or easycrypt calls
proof-ready-for-assistant, pg-custom isn't loaded again.
|
|
Compilation used to run in a separate Emacs process for each file, but that's not
what happens when installing PG with package.el.
|
|
|
|
|
|
|
|
It didn't really matter that these variables were defined and set to nil during
compilation, since we ran compilation in a clean Emacs in --batch mode; it does
matter now, however, since package.el compiles PG in the user's currently
running Emacs instance.
|
|
The PG Makefile does ensure (using --batch) that noninteractive is non-nil while
compiling, but package.el doesn't.
|
|
|
|
|
|
|
|
|
|
|
|
Fix indentation
|
|
* Close ProofGeneral/PG#161.
Issue a "Show" each time a (Uns|S)et Printing is detected (and a proof is open).
|
|
Close ProofGeneral/PG#160
|
|
|
|
- precise tags for definitions
- fix bug with nonempty white space lines
- add several keywords (Proposition, Record, ...)
- generate tags for constructors of inductive definitions
and for record labels
|
|
Fixing #154.
|
|
|
|
|
|
|
|
|
|
While fixing these I discovered several flaws in indentation (what a
suprise). The probem is the following: since we don't have a precise
grammar of tactics, smie often decides that the parent of a sub-part
of a tactic is the previous command instead of the current tacic.
Typical example (fixed now but in general):
foo.
apply bar
with bar'.
Since "apply ... bar'" is considered as one leaf of the grammar, it is
considered to be a child of the previous dot.
.
/\
/ \
foo apply...bar'
Therefore indentation of "with" wants to align with parent "." and
hence with "foo".
Basically we should try to define a much more precise grammar of
complex tactics (with with, as, using etc) in order to fix the
problem. Of course this has the drawback of making impossible to
support user tactic notations.
|
|
|
|
|
|
- infrastructure for saving/resetting customizations not defined
with defpacustom
- improve Coq -> Auto Compilation menu
- polish documentation and manual
|
|
Split coq-par-emergency-cleanup into two functions, one for
reacting on user interrupts and one for cleaning up after
compilation errors.
|
|
see http://proofgeneral.inf.ed.ac.uk/trac/ticket/434, when I
tried to download phox now, no link was working...
|
|
texi2html is dead, see for instance
https://wiki.debian.org/Texi2htmlTransition
|
|
@psteckler I believe you have this patch already in your branch.
|
|
|
