| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2009-11-30 | Fix for Trac #307. | David Aspinall | |
| 2009-11-30 | Replace proof-locked-end -> proof-unprocessed-begin | David Aspinall | |
| 2009-11-28 | Add `proof-script-sticky-error-face' and `proof-sticky-errors' setting. | David Aspinall | |
| 2009-10-15 | proof-script-use-old-parser: remove configuration option and cleanup | David Aspinall | |
| 2009-10-14 | Shorten comments | David Aspinall | |
| 2009-10-03 | proof-script-generic-parse-cmdstart: set case-fold-search | David Aspinall | |
| proof-inside-string: added | |||
| 2009-10-03 | proof-assert-electric-terminator: repair so works at end of buffer | David Aspinall | |
| 2009-10-02 | proof-retract-before-change: give error if prover busy | David Aspinall | |
| (see http://proofgeneral.inf.ed.ac.uk/trac/ticket/293) | |||
| 2009-09-28 | Functions find-and-forget and count-undos now return lists of commands | David Aspinall | |
| 2009-09-25 | pg-toggle-element-visibility: Add back `redraw-frame' call, it *is* | David Aspinall | |
| needed here (possible Emacs bug) | |||
| 2009-09-21 | Remove redisplay function call for Emacs, seems unnecssary. | David Aspinall | |
| 2009-09-21 | Repair some of proof visibility handling | David Aspinall | |
| pg-last-output-displayform: protect against single \n in last output | |||
| 2009-09-20 | proof-script-clear-queue-spans-on-error: jump to start of error span | David Aspinall | |
| (if proof-follow-mode suggests following locked region) | |||
| 2009-09-20 | pg-set-span-helphighlights: add hook to delete help highlight | David Aspinall | |
| on any edit (affects error spans and outdated help spans). | |||
| 2009-09-20 | proof-cmdstart-add-segment-for-cmd: classify all whitespace as a | David Aspinall | |
| comment, not a command. | |||
| 2009-09-16 | pg-last-output-displayform: protect against empty string | David Aspinall | |
| 2009-09-15 | When calling proof-script-preprocess, fix starting position. | David Aspinall | |
| proof-assert-electric-terminator: restore expected behaviour with/without term. | |||
| 2009-09-14 | Fix compile issues | David Aspinall | |
| 2009-09-14 | proof-span-give-warning: no message if inhibit-read-only is set | David Aspinall | |
| 2009-09-14 | Move insert-electric-terminator here. Add experimental error spans. Doc ↵ | David Aspinall | |
| improvements | |||
| 2009-09-10 | Disable debug message in Isar | David Aspinall | |
| 2009-09-10 | Experimental changes to queue several commands at once and to allow ↵ | David Aspinall | |
| pre-processing of commands when they're queued from script | |||
| 2009-09-10 | proof-retract-until-point: protect against finding no span at all | David Aspinall | |
| (mask current bug in Coq code) | |||
| 2009-09-10 | Clean compile | David Aspinall | |
| 2009-09-09 | pg-last-output-displayform: strip trailing CR as well as initial one, | David Aspinall | |
| to tidy up popups for Isabelle. | |||
| 2009-09-09 | Delete the pghelp spans for now, after all. | David Aspinall | |
| 2009-09-09 | proof-script-clear-queue-spans: scan less of buffer | David Aspinall | |
| proof-script-delete-spans: leave 'pghelp spans in place for now pg-set-span-helphighlights: add extra FACE argument proof-done-advancing-save, proof-make-goalsave: support proof-arbitrary-undo-positions. | |||
| 2009-09-09 | proof-shell-error-or-interrupt-seen -> proof-shell-last-error-kind, | David Aspinall | |
| as per previous proof-shell update. | |||
| 2009-09-07 | Fix compile warnings | David Aspinall | |
| 2009-09-06 | pg-add-element: unbound var in debug | David Aspinall | |
| proof-activate-scripting: minor cleanup proof-assert-until-point: don't go back beyond end of locked | |||
| 2009-09-06 | Tweak point movement in `proof-assert-until-point' and | David Aspinall | |
| alter meaning of `proof-only-whitespace-to-locked-region-p'; both now refer to char after point. Script elements are now stored in hash tables rather than lists. | |||
| 2009-09-05 | Minor opt | David Aspinall | |
| 2009-09-05 | proof-set-queue-endpoints: no undo-make-selective-list (pg-protected-undo ↵ | David Aspinall | |
| replaces) proof-done-advancing: remove spurious first case proof-assert-until-point: don't move point, restore intuitive behaviour when on whitespace between unprocessed commands (process preceding commands only) | |||
| 2009-09-05 | Clean whitespace | David Aspinall | |
| 2009-09-05 | Whitespaces and comments | David Aspinall | |
| 2009-09-04 | Add proof-script-evaluate-elisp-comment-regexp security hole. | David Aspinall | |
| 2009-09-04 | proof-file-to-buffer -> find-buffer-visiting | David Aspinall | |
| 2009-09-04 | Remove configuration of obsolete package function-menu (aka "fume") | David Aspinall | |
| 2009-09-04 | Remove configuration of obsolete package function-menu (aka "fume") | David Aspinall | |
| 2009-09-04 | Refactoring point movement commands (in progress). Remove proof-no-command. | David Aspinall | |
| 2009-08-29 | Cleanup of interactive point moving functions (in progress) | David Aspinall | |
| 2009-08-28 | Fix compile warnings | David Aspinall | |
| 2009-08-20 | Doc tweaks via checkdoc. | David Aspinall | |
| 2009-08-20 | proof-one-command-per-line: change default, use in proof-insert-pbp-command. | David Aspinall | |
| 2009-08-17 | Only move proof-overlay-arrow once it's got a position. | David Aspinall | |
| 2009-08-17 | Move the overlay arrow backwards in case of edits above it which | David Aspinall | |
| affect the next position to be processed. | |||
| 2009-08-14 | pg-last-output-displayform: add convenience function | David Aspinall | |
| 2009-08-13 | Add parser cache for proof-segment-up-to. | David Aspinall | |
| 2009-08-07 | proof-colour-locked: complete implementation | David Aspinall | |
| 2009-08-06 | Prevent setting of proof-overlay-arrow if not configured | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |