Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Use `cl-lib` instead of `cl` everywhere | Stefan Monnier | 2018-12-13 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||
* | Update copyright messages and improve the header of elisp files. | Erik Martin-Dorel | 2018-02-21 |
| | |||
* | Remove a few useless eval-and-compile calls | Clément Pit--Claudel | 2017-03-08 |
| | |||
* | Make shell and perl scripts executable. | Erik Martin-Dorel | 2016-09-19 |
| | | | | This addresses part of the issues pointed out in #112 | ||
* | Summary: Don't quote lambda expressions | Stefan Monnier | 2012-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. | ||
* | Replace proof-terminal-char with proof-terminal-string. | David Aspinall | 2010-08-27 |
| | |||
* | lego-shell-adjust-line-width: save-excursion -> with-current-buffer to avoid | David Aspinall | 2010-07-01 |
| | | | | spurious warning in Emacs 23.2 | ||
* | Functions find-and-forget and count-undos now return lists of commands | David Aspinall | 2009-09-28 |
| | |||
* | Set right font-lock-keywords | David Aspinall | 2009-09-10 |
| | |||
* | p-s-classify-output -> p-s-handle-output, and simplify system-specific hook | David Aspinall | 2009-09-09 |
| | |||
* | Remove barely useful proof-shell-abort-goal-regexp (only served to sanitize ↵ | David Aspinall | 2009-09-08 |
| | | | | LEGO messages) | ||
* | lego-shell-process-output -> lego-shell-classify-output | David Aspinall | 2009-09-07 |
| | |||
* | Configuration changes for shell mode revision. | David Aspinall | 2009-09-06 |
| | |||
* | Remove proof-shell-wakeup-char | David Aspinall | 2009-09-06 |
| | |||
* | Clean whitespace | David Aspinall | 2009-09-05 |
| | |||
* | Whitespace and require | David Aspinall | 2009-09-05 |
| | |||
* | Remove proof-shell-prompt-pattern, no longer used. | David Aspinall | 2009-09-04 |
| | |||
* | Remove proof-no-command | David Aspinall | 2009-09-04 |
| | |||
* | Merge changes from Version4Branch. | David Aspinall | 2008-07-24 |
| | |||
* | Docstring with keymap | David Aspinall | 2008-02-17 |
| | |||
* | Updated. | David Aspinall | 2008-01-31 |
| | |||
* | Many compatibility updates, bug fixes, rearrangements for compilation. | David Aspinall | 2008-01-15 |
| | |||
* | Deleted file | David Aspinall | 2007-12-13 |
| | |||
* | Add support for sending back literal commands reusing PBP markup mechanisms. | David Aspinall | 2007-08-14 |
| | |||
* | Disable unicode use on LEGO, uses escape prefix | David Aspinall | 2007-05-10 |
| | |||
* | Deleted file | David Aspinall | 2006-09-22 |
| | |||
* | Changed the type of proof-goal-command-p. It takes now a span, which | Pierre Courtieu | 2006-04-26 |
| | | | | | | allows using a span attribute to detect goal commands. I think I modified all modes accordingly. | ||
* | Fix lego-shell-adjust-line-width for mutliple frame mode. | David Aspinall | 2005-08-14 |
| | |||
* | New files. | David Aspinall | 2004-04-16 |
| | |||
* | Remove X-symbol support from secondary provers temporarily | David Aspinall | 2004-04-14 |
| | |||
* | Make find-and-forget robust for proverproc regions | David Aspinall | 2003-06-05 |
| | |||
* | Fix some compile errors | David Aspinall | 2003-02-24 |
| | |||
* | Improved implementation of zap-commas font lock behaviour, patch from Stefan ↵ | David Aspinall | 2002-08-31 |
| | | | | Monnier | ||
* | Variable name change proof-comment-{start,end}-regexp -> ↵ | David Aspinall | 2002-07-19 |
| | | | | proof-script-comment-{start,end}-regexp. | ||
* | Refactor several variable names; clean up, doc subterm markup and output ↵ | David Aspinall | 2002-07-16 |
| | | | | display. | ||
* | GPL update | David Aspinall | 2002-06-21 |
| | |||
* | Default to /usr/bin/perl | David Aspinall | 2002-06-08 |
| | |||
* | Whitespace | David Aspinall | 2002-01-16 |
| | |||
* | Coq/lego confusion | David Aspinall | 2001-09-09 |
| | |||
* | Add specific install instrs, rearrange. | David Aspinall | 2001-09-03 |
| | |||
* | Change of proof span type back to goalsave | David Aspinall | 2001-08-28 |
| | |||
* | goalsave -> proof | David Aspinall | 2000-12-20 |
| | |||
* | Note about alternative path to perl | David Aspinall | 2000-10-02 |
| | |||
* | Make default path to perl be /usr/bin/perl | David Aspinall | 2000-09-29 |
| | |||
* | Added Uncaught exception errors in coq-error-regexp. | Pierre Courtieu | 2000-09-29 |
| | |||
* | Add Pierre's tweak | David Aspinall | 2000-09-23 |
| | |||
* | basic setup for new indentation code; | Makarius Wenzel | 2000-06-08 |
| | |||
* | Remove spurious requires. | David Aspinall | 2000-06-01 |
| | |||
* | Removed use of proof-terminal-string, added explicit terminators everywhere. | David Aspinall | 2000-05-29 |
| | |||
* | Changed keybindings for lego specific functions | David Aspinall | 2000-05-29 |
| |