Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Update copyright messages and improve the header of elisp files. | 2018-02-21 | |
| | |||
* | Remove a few useless eval-and-compile calls | 2017-03-08 | |
| | |||
* | Summary: Don't quote lambda expressions | 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. | 2010-08-27 | |
| | |||
* | lego-shell-adjust-line-width: save-excursion -> with-current-buffer to avoid | 2010-07-01 | |
| | | | | spurious warning in Emacs 23.2 | ||
* | Functions find-and-forget and count-undos now return lists of commands | 2009-09-28 | |
| | |||
* | Set right font-lock-keywords | 2009-09-10 | |
| | |||
* | p-s-classify-output -> p-s-handle-output, and simplify system-specific hook | 2009-09-09 | |
| | |||
* | Remove barely useful proof-shell-abort-goal-regexp (only served to sanitize ↵ | 2009-09-08 | |
| | | | | LEGO messages) | ||
* | lego-shell-process-output -> lego-shell-classify-output | 2009-09-07 | |
| | |||
* | Configuration changes for shell mode revision. | 2009-09-06 | |
| | |||
* | Remove proof-shell-wakeup-char | 2009-09-06 | |
| | |||
* | Whitespace and require | 2009-09-05 | |
| | |||
* | Remove proof-shell-prompt-pattern, no longer used. | 2009-09-04 | |
| | |||
* | Remove proof-no-command | 2009-09-04 | |
| | |||
* | Merge changes from Version4Branch. | 2008-07-24 | |
| | |||
* | Docstring with keymap | 2008-02-17 | |
| | |||
* | Many compatibility updates, bug fixes, rearrangements for compilation. | 2008-01-15 | |
| | |||
* | Add support for sending back literal commands reusing PBP markup mechanisms. | 2007-08-14 | |
| | |||
* | Disable unicode use on LEGO, uses escape prefix | 2007-05-10 | |
| | |||
* | Changed the type of proof-goal-command-p. It takes now a span, which | 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. | 2005-08-14 | |
| | |||
* | Make find-and-forget robust for proverproc regions | 2003-06-05 | |
| | |||
* | Fix some compile errors | 2003-02-24 | |
| | |||
* | Improved implementation of zap-commas font lock behaviour, patch from Stefan ↵ | 2002-08-31 | |
| | | | | Monnier | ||
* | Variable name change proof-comment-{start,end}-regexp -> ↵ | 2002-07-19 | |
| | | | | proof-script-comment-{start,end}-regexp. | ||
* | Refactor several variable names; clean up, doc subterm markup and output ↵ | 2002-07-16 | |
| | | | | display. | ||
* | GPL update | 2002-06-21 | |
| | |||
* | Change of proof span type back to goalsave | 2001-08-28 | |
| | |||
* | goalsave -> proof | 2000-12-20 | |
| | |||
* | basic setup for new indentation code; | 2000-06-08 | |
| | |||
* | Remove spurious requires. | 2000-06-01 | |
| | |||
* | Removed use of proof-terminal-string, added explicit terminators everywhere. | 2000-05-29 | |
| | |||
* | Changed keybindings for lego specific functions | 2000-05-29 | |
| | |||
* | proof-defass-default -> defpgdefault | 2000-05-26 | |
| | |||
* | Patch for synchronization problem in Coq, perhaps others. | 2000-05-25 | |
| | |||
* | Fix buttons must be 3 long error (for 20.4 compatibility) | 2000-05-16 | |
| | |||
* | Remove proof-assistant-menu-entries, done generically now. | 2000-05-12 | |
| | |||
* | Fix note. | 2000-05-12 | |
| | |||
* | Changes and compatibility fixes for specific menu/keybindings. | 2000-05-11 | |
| | |||
* | Added proof-assistant-keymap and commands for defining insert keys. | 2000-05-02 | |
| | |||
* | Added specific menu for LEGO. | 2000-05-01 | |
| | |||
* | goals-mode -> pbp-mode | 2000-04-07 | |
| | |||
* | Fixed up proof-shell-proof-completed mess nicely. | 2000-04-07 | |
| | |||
* | Fixes for short output duplication problem: set ↵ | 2000-01-06 | |
| | | | | proof-shell-eager-annotation-start-length. | ||
* | Docstring | 1999-11-24 | |
| | |||
* | proof-font-lock-zap-commas=t | 1999-11-15 | |
| | |||
* | proof-nested-goals-allowed -> proof-completed-proof-behaviour | 1999-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. | 1999-11-12 | |
| | |||
* | Changed name of proof-shell-cd-cmd for uniformity. | 1999-10-21 | |
| |