aboutsummaryrefslogtreecommitdiff
path: root/lego
AgeCommit message (Collapse)Author
2018-12-13Use `cl-lib` instead of `cl` everywhereStefan Monnier
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.
2018-02-21Update copyright messages and improve the header of elisp files.Erik Martin-Dorel
2017-03-08Remove a few useless eval-and-compile callsClément Pit--Claudel
2016-09-19Make shell and perl scripts executable.Erik Martin-Dorel
This addresses part of the issues pointed out in #112
2012-08-30Summary: Don't quote lambda expressionsStefan Monnier
* 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.
2010-08-27Replace proof-terminal-char with proof-terminal-string.David Aspinall
2010-07-01lego-shell-adjust-line-width: save-excursion -> with-current-buffer to avoidDavid Aspinall
spurious warning in Emacs 23.2
2009-09-28Functions find-and-forget and count-undos now return lists of commandsDavid Aspinall
2009-09-10Set right font-lock-keywordsDavid Aspinall
2009-09-09p-s-classify-output -> p-s-handle-output, and simplify system-specific hookDavid Aspinall
2009-09-08Remove barely useful proof-shell-abort-goal-regexp (only served to sanitize ↵David Aspinall
LEGO messages)
2009-09-07lego-shell-process-output -> lego-shell-classify-outputDavid Aspinall
2009-09-06Configuration changes for shell mode revision.David Aspinall
2009-09-06Remove proof-shell-wakeup-charDavid Aspinall
2009-09-05Clean whitespaceDavid Aspinall
2009-09-05Whitespace and requireDavid Aspinall
2009-09-04Remove proof-shell-prompt-pattern, no longer used.David Aspinall
2009-09-04Remove proof-no-commandDavid Aspinall
2008-07-24Merge changes from Version4Branch.David Aspinall
2008-02-17Docstring with keymapDavid Aspinall
2008-01-31Updated.David Aspinall
2008-01-15Many compatibility updates, bug fixes, rearrangements for compilation.David Aspinall
2007-12-13Deleted fileDavid Aspinall
2007-08-14Add support for sending back literal commands reusing PBP markup mechanisms.David Aspinall
2007-05-10Disable unicode use on LEGO, uses escape prefixDavid Aspinall
2006-09-22Deleted fileDavid Aspinall
2006-04-26Changed the type of proof-goal-command-p. It takes now a span, whichPierre Courtieu
allows using a span attribute to detect goal commands. I think I modified all modes accordingly.
2005-08-14Fix lego-shell-adjust-line-width for mutliple frame mode.David Aspinall
2004-04-16New files.David Aspinall
2004-04-14Remove X-symbol support from secondary provers temporarilyDavid Aspinall
2003-06-05Make find-and-forget robust for proverproc regionsDavid Aspinall
2003-02-24Fix some compile errorsDavid Aspinall
2002-08-31Improved implementation of zap-commas font lock behaviour, patch from Stefan ↵David Aspinall
Monnier
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-06-21GPL updateDavid Aspinall
2002-06-08Default to /usr/bin/perlDavid Aspinall
2002-01-16WhitespaceDavid Aspinall
2001-09-09Coq/lego confusionDavid Aspinall
2001-09-03Add specific install instrs, rearrange.David Aspinall
2001-08-28Change of proof span type back to goalsaveDavid Aspinall
2000-12-20goalsave -> proofDavid Aspinall
2000-10-02Note about alternative path to perlDavid Aspinall
2000-09-29Make default path to perl be /usr/bin/perlDavid Aspinall
2000-09-29Added Uncaught exception errors in coq-error-regexp.Pierre Courtieu
2000-09-23Add Pierre's tweakDavid Aspinall
2000-06-08basic setup for new indentation code;Makarius Wenzel
2000-06-01Remove spurious requires.David Aspinall
2000-05-29Removed use of proof-terminal-string, added explicit terminators everywhere.David Aspinall
2000-05-29Changed keybindings for lego specific functionsDavid Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:51 +0000