aboutsummaryrefslogtreecommitdiffhomepage
path: root/lego
Commit message (Collapse)AuthorAge
* Use `cl-lib` instead of `cl` everywhereGravatar Stefan Monnier2018-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.Gravatar Erik Martin-Dorel2018-02-21
|
* Remove a few useless eval-and-compile callsGravatar Clément Pit--Claudel2017-03-08
|
* Make shell and perl scripts executable.Gravatar Erik Martin-Dorel2016-09-19
| | | | This addresses part of the issues pointed out in #112
* 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.
* Replace proof-terminal-char with proof-terminal-string.Gravatar David Aspinall2010-08-27
|
* lego-shell-adjust-line-width: save-excursion -> with-current-buffer to avoidGravatar David Aspinall2010-07-01
| | | | spurious warning in Emacs 23.2
* Functions find-and-forget and count-undos now return lists of commandsGravatar David Aspinall2009-09-28
|
* Set right font-lock-keywordsGravatar David Aspinall2009-09-10
|
* p-s-classify-output -> p-s-handle-output, and simplify system-specific hookGravatar David Aspinall2009-09-09
|
* Remove barely useful proof-shell-abort-goal-regexp (only served to sanitize ↵Gravatar David Aspinall2009-09-08
| | | | LEGO messages)
* lego-shell-process-output -> lego-shell-classify-outputGravatar David Aspinall2009-09-07
|
* Configuration changes for shell mode revision.Gravatar David Aspinall2009-09-06
|
* Remove proof-shell-wakeup-charGravatar David Aspinall2009-09-06
|
* Clean whitespaceGravatar David Aspinall2009-09-05
|
* Whitespace and requireGravatar David Aspinall2009-09-05
|
* Remove proof-shell-prompt-pattern, no longer used.Gravatar David Aspinall2009-09-04
|
* Remove proof-no-commandGravatar David Aspinall2009-09-04
|
* Merge changes from Version4Branch.Gravatar David Aspinall2008-07-24
|
* Docstring with keymapGravatar David Aspinall2008-02-17
|
* Updated.Gravatar David Aspinall2008-01-31
|
* Many compatibility updates, bug fixes, rearrangements for compilation.Gravatar David Aspinall2008-01-15
|
* Deleted fileGravatar David Aspinall2007-12-13
|
* Add support for sending back literal commands reusing PBP markup mechanisms.Gravatar David Aspinall2007-08-14
|
* Disable unicode use on LEGO, uses escape prefixGravatar David Aspinall2007-05-10
|
* Deleted fileGravatar David Aspinall2006-09-22
|
* Changed the type of proof-goal-command-p. It takes now a span, whichGravatar Pierre Courtieu2006-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.Gravatar David Aspinall2005-08-14
|
* New files.Gravatar David Aspinall2004-04-16
|
* Remove X-symbol support from secondary provers temporarilyGravatar David Aspinall2004-04-14
|
* Make find-and-forget robust for proverproc regionsGravatar David Aspinall2003-06-05
|
* Fix some compile errorsGravatar David Aspinall2003-02-24
|
* Improved implementation of zap-commas font lock behaviour, patch from Stefan ↵Gravatar David Aspinall2002-08-31
| | | | Monnier
* Variable name change proof-comment-{start,end}-regexp -> ↵Gravatar David Aspinall2002-07-19
| | | | proof-script-comment-{start,end}-regexp.
* Refactor several variable names; clean up, doc subterm markup and output ↵Gravatar David Aspinall2002-07-16
| | | | display.
* GPL updateGravatar David Aspinall2002-06-21
|
* Default to /usr/bin/perlGravatar David Aspinall2002-06-08
|
* WhitespaceGravatar David Aspinall2002-01-16
|
* Coq/lego confusionGravatar David Aspinall2001-09-09
|
* Add specific install instrs, rearrange.Gravatar David Aspinall2001-09-03
|
* Change of proof span type back to goalsaveGravatar David Aspinall2001-08-28
|
* goalsave -> proofGravatar David Aspinall2000-12-20
|
* Note about alternative path to perlGravatar David Aspinall2000-10-02
|
* Make default path to perl be /usr/bin/perlGravatar David Aspinall2000-09-29
|
* Added Uncaught exception errors in coq-error-regexp.Gravatar Pierre Courtieu2000-09-29
|
* Add Pierre's tweakGravatar David Aspinall2000-09-23
|
* basic setup for new indentation code;Gravatar Makarius Wenzel2000-06-08
|
* Remove spurious requires.Gravatar David Aspinall2000-06-01
|
* Removed use of proof-terminal-string, added explicit terminators everywhere.Gravatar David Aspinall2000-05-29
|
* Changed keybindings for lego specific functionsGravatar David Aspinall2000-05-29
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-01 18:33:13 +0000