proof-general/phox, branch master Emacs plugins for proof management systems Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev. 2018-12-16T03:55:12+00:00 Stefan Monnier 2018-12-16T01:03:43+00:00 1854459fef368dfc8ca870792e7e3b065a2241c6 Fix a few more cl.el leftovers. Get rid of remaining use of iso-2022. Use SMIE unconditionally. * coq/coq-abbrev.el: Use lexical-binding. (coq-install-abbrevs): Delete, only keep the relevant contents. (proof-defstringset-fn): Remove. Fold changes into the main version. * coq/coq-indent.el (coq-find-real-start): Use forward-comment. * coq/coq-smie.el: Use lexical-binding. Assume `smie` is available. (coq--string-suffix-p): Rename from coq-string-suffix-p. Use string-suffix-p for it when available. (string-suffix-p): Never define here. Change all users to use coq--string-suffix-p instead. (coq-smie-.-deambiguate): Use forward-comment. Remove unused var `beg`. (coq-backward-token-fast-nogluing-dot-friends) (coq-forward-token-fast-nogluing-dot-friends): Remove unused var `tok-other`. (coq-smie-search-token-backward): Remove unused var `p`. (coq-smie-:=-deambiguate, coq-smie-backward-token): Prefer char-before over looking-back. (coq-smie-rules): Use `pcase` over deprecated cl's `case`. * coq/coq-syntax.el: Use lexical-binding. (coq-count-match): Rewrite so it doesn't do needless heap-allocation. (coq-module-opening-p, coq-section-command-p, coq-goal-command-str-p): Use case-fold-search rather than proof-string-match. (coq-goal-command-regexp): Forward-declare. (coq-save-command-regexp-strict): Move before first use. (coq-reserved-regexp): Use a single \_< ... \_>. (coq-detect-hyps-positions): Limit search for looking-back. * coq/coq.el: Remove SMIE declarations since SMIE is always used. (coq-use-smie): Remove, unused. (coq-smie): Always require. * generic/pg-pbrpm.el: Fix leftover cl.el uses. * generic/proof-utils.el (proof-defstringset-fn): Fix copy&paste error in the docstring, improve interactive prompt. * lib/maths-menu.el: Use utf-8 and lexical-binding. 
Fix a few more cl.el leftovers.  Get rid of remaining use of iso-2022.
Use SMIE unconditionally.

* coq/coq-abbrev.el: Use lexical-binding.
(coq-install-abbrevs): Delete, only keep the relevant contents.
(proof-defstringset-fn): Remove.  Fold changes into the main version.

* coq/coq-indent.el (coq-find-real-start): Use forward-comment.

* coq/coq-smie.el: Use lexical-binding.  Assume `smie` is available.
(coq--string-suffix-p): Rename from coq-string-suffix-p.
Use string-suffix-p for it when available.
(string-suffix-p): Never define here.  Change all users to use
coq--string-suffix-p instead.
(coq-smie-.-deambiguate): Use forward-comment.  Remove unused var `beg`.
(coq-backward-token-fast-nogluing-dot-friends)
(coq-forward-token-fast-nogluing-dot-friends): Remove unused var
`tok-other`.
(coq-smie-search-token-backward): Remove unused var `p`.
(coq-smie-:=-deambiguate, coq-smie-backward-token): Prefer char-before
over looking-back.
(coq-smie-rules): Use `pcase` over deprecated cl's `case`.

* coq/coq-syntax.el: Use lexical-binding.
(coq-count-match): Rewrite so it doesn't do needless heap-allocation.
(coq-module-opening-p, coq-section-command-p, coq-goal-command-str-p):
Use case-fold-search rather than proof-string-match.
(coq-goal-command-regexp): Forward-declare.
(coq-save-command-regexp-strict): Move before first use.
(coq-reserved-regexp): Use a single \_< ... \_>.
(coq-detect-hyps-positions): Limit search for looking-back.

* coq/coq.el: Remove SMIE declarations since SMIE is always used.
(coq-use-smie): Remove, unused.
(coq-smie): Always require.

* generic/pg-pbrpm.el: Fix leftover cl.el uses.

* generic/proof-utils.el (proof-defstringset-fn): Fix copy&paste error
in the docstring, improve interactive prompt.

* lib/maths-menu.el: Use utf-8 and lexical-binding.
Add link to the latex-pretty-symbols package mentioned by @craff 2018-08-22T23:23:32+00:00 Erik Martin-Dorel 2018-08-22T22:01:38+00:00 fd4ab1df3c55ea29e984d934f482bf9cc1966c9d Fix the typo reported by @siddharthist as well 
Fix the typo reported by @siddharthist as well
Fix most doc issues raised by (checkdoc) 2018-08-22T23:23:31+00:00 Erik Martin-Dorel 2018-08-22T22:01:12+00:00 86d22428959a0f5aecef270e0f4dd7d4b5712fc3 






phox syntax table + more symbols
2017-09-22T04:55:26+00:00

Christophe Raffalli

2017-09-22T04:55:26+00:00

7ee9486a616b12ea99490b134c1417792ef78459












phox is back
2017-09-21T22:28:27+00:00

Christophe Raffalli

2017-09-21T22:28:27+00:00

06d72fb68fd9dd57632650f1a79de01317a6069f












Change (eval-when (compile) ...) to (eval-when-compile ...)
2017-05-05T16:10:58+00:00

Clément Pit--Claudel

2017-05-05T16:08:54+00:00

574b0992e3cb4b7a4ad88400b9a5ab0198a96ca5

This fixes a bunch of compilation warnings





This fixes a bunch of compilation warnings







Fix incorrect uses of defvar
2017-03-08T20:06:17+00:00

Clément Pit--Claudel

2017-02-26T00:06:26+00:00

33614d35a25b54c23171c360a61b913f0c1158ce

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.





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.







Summary: Fix compile warning on phox-toolbar-entries
2015-03-05T09:47:06+00:00

David Aspinall

2015-03-05T09:47:06+00:00

cffda98288d59860f7744d78de2efc3b8ff410b9












Fix compile error with make-face
2015-03-05T09:31:40+00:00

David Aspinall

2015-03-05T09:31:40+00:00

d8fb118d2012a4325118f51a51b28b12661b1789












Summary: Don't quote lambda expressions
2012-08-30T14:30:23+00:00

Stefan Monnier

2012-08-30T14:30:23+00:00

0d0af3dcce3a9b29d9c33c4cee34ca5249713904

* 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.





* 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.