aboutsummaryrefslogtreecommitdiffhomepage
path: root/phox
Commit message (Collapse)AuthorAge
* Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev.Gravatar Stefan Monnier2018-12-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 @craffGravatar Erik Martin-Dorel2018-08-23
| | | | Fix the typo reported by @siddharthist as well
* Fix most doc issues raised by (checkdoc)Gravatar Erik Martin-Dorel2018-08-23
|
* phox syntax table + more symbolsGravatar Christophe Raffalli2017-09-22
|
* phox is backGravatar Christophe Raffalli2017-09-22
|
* Change (eval-when (compile) ...) to (eval-when-compile ...)Gravatar Clément Pit--Claudel2017-05-05
| | | | This fixes a bunch of compilation warnings
* Fix incorrect uses of defvarGravatar Clément Pit--Claudel2017-03-08
| | | | | | | 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-entriesGravatar David Aspinall2015-03-05
|
* Fix compile error with make-faceGravatar David Aspinall2015-03-05
|
* Summary: Don't quote lambda expressionsGravatar Stefan Monnier2012-08-30
| | | | | | | | | | | | | | | | * 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.
* Fix compile error, Trac #437.Gravatar David Aspinall2012-04-06
|
* Outline required compile and runGravatar David Aspinall2011-10-17
|
* Replace proof-terminal-char with proof-terminal-string.Gravatar David Aspinall2010-08-27
|
* phox-find-and-forget: return a listGravatar David Aspinall2009-09-29
|
* Prevent many compile warningsGravatar David Aspinall2009-09-15
|
* Some fixes to requires etcGravatar David Aspinall2009-09-10
|
* Tidy whitespaceGravatar David Aspinall2009-09-05
|
* resp-font-lock-keywords -> response-font-lock-keywords; ↵Gravatar David Aspinall2009-09-05
| | | | output-fontify-enable removed
* Remove proof-shell-prompt-pattern, no longer used.Gravatar David Aspinall2009-09-04
|
* Remove proof-no-commandGravatar David Aspinall2009-09-04
|
* Remove (commented out) x-symbol configurationGravatar David Aspinall2009-09-01
|
* hack with phox-prog-name and phox-prog-name-guess to have this phox folder ↵Gravatar Christophe Raffalli2009-09-01
| | | | working with PG 3.7
* Removed support for x-symbol (I do not like it because it changes the buffer ↵Gravatar Christophe Raffalli2009-09-01
| | | | | | | | content !) sym-lock is still available on xemacs only various other bug fix.
* Merge changes from Version4Branch.Gravatar David Aspinall2008-07-24
|
* Docstring with keymapGravatar David Aspinall2008-02-17
|
* Updated.Gravatar David Aspinall2008-01-31
|
* Remove use of proof-assGravatar David Aspinall2008-01-24
|
* Compilation tweaksGravatar David Aspinall2008-01-16
|
* Many compatibility updates, bug fixes, rearrangements for compilation.Gravatar David Aspinall2008-01-15
|
* Prevent compile error on atomic-extentsGravatar David Aspinall2007-12-14
|
* Protect usage of list-fonts, unknown functionGravatar David Aspinall2007-12-10
|
* back to using sym-lock ... x-symbol will not be supported anymore for PhoX + ↵Gravatar Christophe Raffalli2006-02-24
| | | | imporvment in proof by contextual menu
* bug fixGravatar Christophe Raffalli2005-10-20
|
* added lock and unlock for unification variablesGravatar Christophe Raffalli2005-10-12
|
* *** empty log message ***Gravatar Christophe Raffalli2005-07-05
|
* New files.Gravatar David Aspinall2005-03-25
|
* Attempt to address X-Symbol startup problems for PhoX.Gravatar David Aspinall2005-02-13
|
* *** empty log message ***Gravatar Christophe Raffalli2005-02-09
|
* changes to pbrpmGravatar Christophe Raffalli2004-12-08
|
* work on proof by contextual menu for phoxGravatar Christophe Raffalli2004-11-22
|
* replaced root2.phx by new square-root-2.phxGravatar Christophe Raffalli2004-10-20
|
* improvment of phox-x-symbol, supress sym-lock, first support for proof by ↵Gravatar Christophe Raffalli2004-10-20
| | | | contextual menu
* first try to make x-symbol worksGravatar Christophe Raffalli2004-05-17
|
* *** empty log message ***Gravatar Christophe Raffalli2004-04-16
|
* New files.Gravatar David Aspinall2004-04-16
|
* Updated.Gravatar David Aspinall2004-04-14
|
* Fix compiler warningsGravatar David Aspinall2004-03-01
|
* Remove non-existent proof-state-command settingGravatar David Aspinall2004-03-01
|
* updating for new PG versionGravatar Christophe Raffalli2004-01-30
|
* Make find-and-forget robust for proverproc regionsGravatar David Aspinall2003-06-05
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 17:55:55 +0000