aboutsummaryrefslogtreecommitdiff
path: root/phox/phox.el
AgeCommit message (Collapse)Author
2018-12-15Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev.Stefan Monnier
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.
2018-08-23Add link to the latex-pretty-symbols package mentioned by @craffErik Martin-Dorel
Fix the typo reported by @siddharthist as well
2018-08-23Fix most doc issues raised by (checkdoc)Erik Martin-Dorel
2017-09-22phox syntax table + more symbolsChristophe Raffalli
2017-09-22phox is backChristophe Raffalli
2017-03-08Fix incorrect uses of defvarClément Pit--Claudel
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.
2015-03-05Summary: Fix compile warning on phox-toolbar-entriesDavid Aspinall
2010-08-27Replace proof-terminal-char with proof-terminal-string.David Aspinall
2009-09-15Prevent many compile warningsDavid Aspinall
2009-09-10Some fixes to requires etcDavid Aspinall
2009-09-05resp-font-lock-keywords -> response-font-lock-keywords; ↵David Aspinall
output-fontify-enable removed
2009-09-04Remove proof-shell-prompt-pattern, no longer used.David Aspinall
2009-09-01Remove (commented out) x-symbol configurationDavid Aspinall
2009-09-01hack with phox-prog-name and phox-prog-name-guess to have this phox folder ↵Christophe Raffalli
working with PG 3.7
2009-09-01Removed support for x-symbol (I do not like it because it changes the buffer ↵Christophe Raffalli
content !) sym-lock is still available on xemacs only various other bug fix.
2008-07-24Merge changes from Version4Branch.David Aspinall
2008-02-17Docstring with keymapDavid Aspinall
2008-01-24Remove use of proof-assDavid Aspinall
2008-01-15Many compatibility updates, bug fixes, rearrangements for compilation.David Aspinall
2006-02-24back to using sym-lock ... x-symbol will not be supported anymore for PhoX + ↵Christophe Raffalli
imporvment in proof by contextual menu
2005-10-20bug fixChristophe Raffalli
2005-07-05*** empty log message ***Christophe Raffalli
2005-02-13Attempt to address X-Symbol startup problems for PhoX.David Aspinall
2005-02-09*** empty log message ***Christophe Raffalli
2004-12-08changes to pbrpmChristophe Raffalli
2004-11-22work on proof by contextual menu for phoxChristophe Raffalli
2004-10-20improvment of phox-x-symbol, supress sym-lock, first support for proof by ↵Christophe Raffalli
contextual menu
2004-05-17first try to make x-symbol worksChristophe Raffalli
2004-04-16*** empty log message ***Christophe Raffalli
2004-03-01Remove non-existent proof-state-command settingDavid Aspinall
2003-02-15Fixes so that compile worksDavid Aspinall
2003-02-12change for version 0.83 of PhoXChristophe Raffalli
2002-07-25change to support version 4.4 of x-symbolChristophe Raffalli
2002-07-19Variable name change proof-comment-{start,end}-regexp -> ↵David Aspinall
proof-script-comment-{start,end}-regexp.
2002-07-16Refactor several variable names; clean up, doc subterm markup and output ↵David Aspinall
display.
2002-03-21added hook: proof-before-fontify-output-hookChristophe Raffalli
2002-03-05*** empty log message ***Christophe Raffalli
2001-07-25Various changes for win32 compatibilityChristophe Raffalli
2001-06-22*** empty log message ***Christophe Raffalli
2001-02-20*** empty log message ***Christophe Raffalli
2001-02-20*** empty log message ***Christophe Raffalli
2001-02-07*** empty log message ***Christophe Raffalli
2001-02-07*** empty log message ***Christophe Raffalli
2001-02-01*** empty log message ***Christophe Raffalli
2001-01-18*** empty log message ***Christophe Raffalli
2001-01-11*** empty log message ***Christophe Raffalli
2000-12-22*** empty log message ***Christophe Raffalli
2000-12-22*** empty log message ***Christophe Raffalli
2000-12-22*** empty log message ***Christophe Raffalli
2000-12-22*** empty log message ***Christophe Raffalli
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:17:09 +0000