| Age | Commit message (Collapse) | Author |
|---|
|
This fix is not completely satisfying for the following reason:
1- I had to add a new hook in generic code. But I don't see how we
could avoid this: the computation of options must happen AFTER the
proof-prog-name is asked to the user, because this computation
depends on the version of coq.
2- We should fix the synchronization between coq-prog-name and
proof-prog-name. Either remove coq-prog-name and use only
proof-prog-name, or have the generic coq always point to
some (proof-ass-sym prog-name).
|
|
Use lexical-binding in a few files where it was easy.
Don't require `proof-compat` when it's not used.
* coq/coq-db.el: Use lexical-binding.
* coq/coq-system.el: Use lexical-binding.
(coq--extract-prog-args): Use concatenated-args rather than recomputing it.
* coq/coq.el: Require `span` to silence some warnings.
* generic/pg-user.el: Use lexical-binding.
(complete, add-completion, completion-min-length): Silence warnings.
* generic/pg-xml.el: Use lexical-binding.
(pg-xml-string-of): Prefer mapconcat to reduce+concat.
* generic/proof-depends.el: Use lexical-binding.
(proof-dep-split-deps): Use `push`.
* generic/proof-shell.el: Require `span` to silence some warnings.
(proof-shell-invisible-command): Don't use lexical-let just to build
a wasteful η-redex!
* lib/holes.el: Use lexical-binding.
Remove redundant :group args.
* lib/span.el: Use lexical-binding.
(span-read-only-hook): Use user-error.
(span-raise): Remove, unused.
|
|
Move `defvar`s used to silence warnings outside of eval-when-compile.
Make sure they don't actually give a value to the var.
* pg-init.el: Simplify.
Use (if t ...) to avoid running `require` at compile-time.
Don't add subdirs to load-path here since this code is never used.
(pg-init--script-full-path, pg-init--pg-root):
Inline their definition into their sole user.
* generic/proof-utils.el (proof-resize-window-tofit):
Inline definitions of window-leftmost-p and window-rightmost-p previously
in proof-compat.el.
* lib/proof-compat.el (proof-running-on-win32): Remove, not used.
(mac-key-mode): Remove, there's no carbon-emacs-package-version in
Emacs≥24.3.
(pg-custom-undeclare-variable): Use dolist.
(save-selected-frame): Remove, save-selected-window also saves&restores
the selected frame at the same time. Update all users (which already
used save-selected-window around it).
(window-leftmost-p, window-rightmost-p, window-bottom-p)
(find-coding-system): Remove, unused.
* hol-light/hol-light.el (caml-font-lock-keywords): Don't try to defvar
it to a dummy value and...
(hol-light): ...check its existence before using it instead.
* coq/coq.el (coq-may-use-prettify): Simplify initialization.
|
|
|
|
Fixes GH-386.
Reported-by: @mrkkrp
|
|
Fix #158 by extending helpspan
|
|
|
|
|
|
This commit ensures the version number is (version-to-list)-compliant.
|
|
Update phox support
|
|
|
|
|
|
Close ProofGeneral/PG#31
|
|
|
|
This commit address ProofGeneral/PG#193.
|
|
Without the string-end regexp matches all the file names which match the regexp
`.eca?`.
|
|
|
|
|
|
This fixes a bunch of compilation warnings
|
|
[WIP] ELPA/MELPA support
|
|
|
|
|
|
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'.
|
|
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#160
|
|
|
|
|
|
|
|
|
|
- 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...
|
|
EasyCrypt PG mode
|
|
In Coq 8.6 evar status printing is off by default, causing
prooftree to crash. This patch inserts invisible commands to
switch evar status printing on and off. This is done via the
urgent-action-hook.
|
|
|
|
|
|
|
|
|
|
Keep going
|
|
Remove default absolute name from coq-prog-name (Fixes #76), but keep displaying…
|
|
when asking for it.
|
|
With this option set, compilation continues after the first error
to compile as much as possible and to potentially report more
than one error.
|
|
|
|
|
|
|
