aboutsummaryrefslogtreecommitdiffhomepage
path: root/lego/lego.el
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
|
* 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
|
* 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
|
* Many compatibility updates, bug fixes, rearrangements for compilation.Gravatar David Aspinall2008-01-15
|
* 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
|
* 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
|
* 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
|
* Change of proof span type back to goalsaveGravatar David Aspinall2001-08-28
|
* goalsave -> proofGravatar David Aspinall2000-12-20
|
* 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
|
* proof-defass-default -> defpgdefaultGravatar David Aspinall2000-05-26
|
* Patch for synchronization problem in Coq, perhaps others.Gravatar David Aspinall2000-05-25
|
* Fix buttons must be 3 long error (for 20.4 compatibility)Gravatar David Aspinall2000-05-16
|
* Remove proof-assistant-menu-entries, done generically now.Gravatar David Aspinall2000-05-12
|
* Fix note.Gravatar David Aspinall2000-05-12
|
* Changes and compatibility fixes for specific menu/keybindings.Gravatar David Aspinall2000-05-11
|
* Added proof-assistant-keymap and commands for defining insert keys.Gravatar David Aspinall2000-05-02
|
* Added specific menu for LEGO.Gravatar David Aspinall2000-05-01
|
* goals-mode -> pbp-modeGravatar David Aspinall2000-04-07
|
* Fixed up proof-shell-proof-completed mess nicely.Gravatar David Aspinall2000-04-07
|
* Fixes for short output duplication problem: set ↵Gravatar David Aspinall2000-01-06
| | | | proof-shell-eager-annotation-start-length.
* DocstringGravatar David Aspinall1999-11-24
|
* proof-font-lock-zap-commas=tGravatar David Aspinall1999-11-15
|
* proof-nested-goals-allowed -> proof-completed-proof-behaviourGravatar David Aspinall1999-11-14
| | | | | Patch for more flexible handling of closing goal...save regions after proof has been completed.
* Set font-lock-keywords before calling proof-config-done.Gravatar David Aspinall1999-11-12
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 01:40:48 +0000