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. | ||
* | Cleanup patch; Moving defvar to toplevel | Stefan Monnier | 2018-12-12 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Move `defvar`s used to silence warnings outside of eval-when-compile. Make sure they don't actually give a value to the var. * pg-init.el: Simplify. Use (if t ...) to avoid running `require` at compile-time. Don't add subdirs to load-path here since this code is never used. (pg-init--script-full-path, pg-init--pg-root): Inline their definition into their sole user. * generic/proof-utils.el (proof-resize-window-tofit): Inline definitions of window-leftmost-p and window-rightmost-p previously in proof-compat.el. * lib/proof-compat.el (proof-running-on-win32): Remove, not used. (mac-key-mode): Remove, there's no carbon-emacs-package-version in Emacs≥24.3. (pg-custom-undeclare-variable): Use dolist. (save-selected-frame): Remove, save-selected-window also saves&restores the selected frame at the same time. Update all users (which already used save-selected-window around it). (window-leftmost-p, window-rightmost-p, window-bottom-p) (find-coding-system): Remove, unused. * hol-light/hol-light.el (caml-font-lock-keywords): Don't try to defvar it to a dummy value and... (hol-light): ...check its existence before using it instead. * coq/coq.el (coq-may-use-prettify): Simplify initialization. | ||
* | Fix most doc issues raised by (checkdoc) | Erik Martin-Dorel | 2018-08-23 |
| | |||
* | Update copyright messages and improve the header of elisp files. | Erik Martin-Dorel | 2018-02-21 |
| | |||
* | Fix pg-{show,hide}-all-proofs and Move them into pg-user.el. | Erik Martin-Dorel | 2017-08-15 |
| | | | | This commit address ProofGeneral/PG#193. | ||
* | Fix incorrect assumption that noninteractive == byte-compiling | Clément Pit--Claudel | 2017-03-08 |
| | | | | | The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't. | ||
* | Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta). | Erik Martin-Dorel | 2016-07-04 |
| | |||
* | Summary: Compile warning on speedbar-add-supported-extension | David Aspinall | 2015-03-13 |
| | |||
* | Summary: Fix for bug #489 (make p-electric-terminator-enable appear as minor ↵ | David Aspinall | 2015-03-13 |
| | | | | mode) | ||
* | Don't mess with overlay priorities. | Stefan Monnier | 2014-06-06 |
| | |||
* | Add user option proof-next-command-insert-space. | David Aspinall | 2012-08-14 |
| | |||
* | * generic/pg-user.el (which-func-modes): Fix compiler declaration. | Stefan Monnier | 2012-06-29 |
| | | | | * generic/proof-site.el (assistants): Fix regexp. | ||
* | Summary: Handle the new t value of which-func-modes. | Stefan Monnier | 2012-06-08 |
| | |||
* | let proof-retract-buffer only move point when called interactively | Hendrik Tews | 2012-05-31 |
| | |||
* | Remove dependency of pg-movie on pg-user | David Aspinall | 2011-10-17 |
| | |||
* | proof-electric-terminator: allow a prefix argument to avoid electric action. | David Aspinall | 2011-09-14 |
| | | | | Addresses Trac #422 | ||
* | proof-undo-and-delete-last-successful-command: obey spec (Trac #407) | David Aspinall | 2011-06-03 |
| | |||
* | Improve hint messages; use proof mode keymap. | David Aspinall | 2011-01-31 |
| | |||
* | pg-create-in-span-context-menu: remove "Move up" and "Move down". | David Aspinall | 2011-01-19 |
| | | | | These don't seem to be very useful or reliable. | ||
* | pg-span-context-menu: add doc | David Aspinall | 2010-10-10 |
| | |||
* | Clean up obsolete comments | David Aspinall | 2010-10-04 |
| | |||
* | Fixes in strings/comments from Erik Martin-Dorel | David Aspinall | 2010-10-04 |
| | |||
* | Add doc | David Aspinall | 2010-10-01 |
| | |||
* | proof-script-new-command-advance: add back some indentation attempt | David Aspinall | 2010-10-01 |
| | | | | | auto sending: improve messages, bind autosend-running flag lexically in case of errors query identifier: use history variable, remove key bindings | ||
* | proof-undo-and-delete-last-successful-command: repair (after | David Aspinall | 2010-09-22 |
| | | | | proof-retract-until-point changed type). | ||
* | proof-autosend-loop: adjust to only update modified tick when sending | David Aspinall | 2010-09-21 |
| | | | | (engages autosend slightly more often, but not quite often enough) | ||
* | Comments | David Aspinall | 2010-09-08 |
| | |||
* | Remove proof-autosend-error-point | David Aspinall | 2010-08-27 |
| | |||
* | Implement the eagerly anticipated Beyond Script Management Feature No.2 ↵ | David Aspinall | 2010-08-27 |
| | | | | (i.e., automatic preview of next command) | ||
* | Tidy comments | David Aspinall | 2010-08-24 |
| | |||
* | Prevent electric terminator modeline effect in non proof script modes. | David Aspinall | 2010-08-23 |
| | |||
* | Add Fast Process Buffer option | David Aspinall | 2010-08-19 |
| | |||
* | proof-autosend-loop: don't enter if shell is already busy processing | David Aspinall | 2010-08-18 |
| | |||
* | Style fix in messages | David Aspinall | 2010-08-18 |
| | |||
* | Autosend: don't autosend after undoing; add proof-shell-last-queuemode to ↵ | David Aspinall | 2010-08-17 |
| | | | | support this. | ||
* | autosend loop: wait for shell after sending interrupt (ensures output processing | David Aspinall | 2010-08-17 |
| | | | | happens when proof-autosend-running is set). | ||
* | Note about fix required to proof-autosend-error-point | David Aspinall | 2010-08-17 |
| | |||
* | Autosend: prevent repeatedly sending erroneous commands (in progress) | David Aspinall | 2010-08-17 |
| | |||
* | Fix compile errors, update tags | David Aspinall | 2010-08-16 |
| | |||
* | proof-issue-new-command: remove spurious goto-char (ref Trac #330) | David Aspinall | 2010-08-15 |
| | |||
* | Preliminary and experimental support for automatically sending commands. | David Aspinall | 2010-08-15 |
| | |||
* | Checkdoc cleanups | David Aspinall | 2010-08-08 |
| | |||
* | pg-protected-undo: remove separate `proof-allow-undo-in-read-only' and | David Aspinall | 2010-08-03 |
| | | | | | make consistent with `proof-strict-read-only' setting. In particular, if "Edit Freely" is selected then we don't do any retraction. | ||
* | Add pg-protected-undo improved version due to Erik Martin-Dorel | David Aspinall | 2010-08-02 |
| | |||
* | Cleanups for save-excursion to avoid warnings in latest Emacs versions | David Aspinall | 2010-07-08 |
| | |||
* | Rework script span element hiding to avoid buffer-invisibility-spec. Add ↵ | David Aspinall | 2009-12-03 |
| | | | | command elements. | ||
* | Replace proof-locked-end -> proof-unprocessed-begin | David Aspinall | 2009-11-30 |
| | |||
* | Whitespace | David Aspinall | 2009-10-14 |
| | |||
* | proof-electric-terminator: check if inside a string/comment. | David Aspinall | 2009-10-03 |
| | |||
* | Clean up hints about buffer display | David Aspinall | 2009-09-29 |
| |