| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
This fixes a bunch of compilation warnings
|
| |
|
|
|
| |
Compilation used to run in a separate Emacs process for each file, but that's not
what happens when installing PG with package.el.
|
| |
|
|
|
| |
The PG Makefile does ensure (using --batch) that noninteractive is non-nil while
compiling, but package.el doesn't.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* coq/coq-indent.el (coq-indent-inner-regexp): Remove old X-Symbol element.
(coq-save-count, coq-proof-count):
* obsolete/plastic/plastic.el (plastic-shell-handle-output):
* lib/texi-docstring-magic.el (texi-docstring-magic-insert-magic):
* lib/pg-dev.el (emacs-lisp-mode-hook):
* lib/maths-menu.el (maths-menu-filter-predicate)
(maths-menu-tokenise-insert):
* lib/holes.el (holes-next):
* lego/lego.el (lego-shell-handle-output):
* isar/isabelle-system.el (isabelle-docs-menu):
* coq/coq.el (coq-compile-command, coq-compile-auto-save)
(coq-compile-ignored-directories, coq-load-path-safep)
(proof-shell-handle-delayed-output-hook): Don't quote lambda.
|
| | |
|
| | |
|
| |
|
|
| |
interactive-p with called-interactively-p)
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
pre-processing of commands when they're queued from script
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
ISABELLE_PROCESS refers to "isabelle-process";
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
change. Also logic menu tooltips.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
breaks Poly/MK 5;
|
| |
|
Stefan Monnier
Clément Pit--Claudel
David Aspinall
Makarius Wenzel