aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-script.el
AgeCommit message (Expand)Author
2010-08-08proof-assert-electric-terminator: give more user-friendly error message if un...David Aspinall
2010-08-08Checkdoc cleanupsDavid Aspinall
2010-08-03proof-assert-electric-terminator: fix logic for inserting at buffer endDavid Aspinall
2010-08-03Move key binding for proof assistant keymap (fixes compilation bug)David Aspinall
2010-08-03save-some-buffers: only offer to save proof script buffersDavid Aspinall
2010-08-03Add support for basic "movie" recording. See http://mws.cs.ru.nl/proviola.David Aspinall
2010-07-08Cleanups for save-excursion to avoid warnings in latest Emacs versionsDavid Aspinall
2009-12-03Rework script span element hiding to avoid buffer-invisibility-spec. Add com...David Aspinall
2009-11-30Fix for Trac #307.David Aspinall
2009-11-30Replace proof-locked-end -> proof-unprocessed-beginDavid Aspinall
2009-11-28Add `proof-script-sticky-error-face' and `proof-sticky-errors' setting.David Aspinall
2009-10-15proof-script-use-old-parser: remove configuration option and cleanupDavid Aspinall
2009-10-14Shorten commentsDavid Aspinall
2009-10-03proof-script-generic-parse-cmdstart: set case-fold-searchDavid Aspinall
2009-10-03proof-assert-electric-terminator: repair so works at end of bufferDavid Aspinall
2009-10-02proof-retract-before-change: give error if prover busyDavid Aspinall
2009-09-28Functions find-and-forget and count-undos now return lists of commandsDavid Aspinall
2009-09-25pg-toggle-element-visibility: Add back `redraw-frame' call, it *is*David Aspinall
2009-09-21Remove redisplay function call for Emacs, seems unnecssary.David Aspinall
2009-09-21Repair some of proof visibility handlingDavid Aspinall
2009-09-20proof-script-clear-queue-spans-on-error: jump to start of error spanDavid Aspinall
2009-09-20pg-set-span-helphighlights: add hook to delete help highlightDavid Aspinall
2009-09-20proof-cmdstart-add-segment-for-cmd: classify all whitespace as aDavid Aspinall
2009-09-16pg-last-output-displayform: protect against empty stringDavid Aspinall
2009-09-15When calling proof-script-preprocess, fix starting position.David Aspinall
2009-09-14Fix compile issuesDavid Aspinall
2009-09-14proof-span-give-warning: no message if inhibit-read-only is setDavid Aspinall
2009-09-14Move insert-electric-terminator here. Add experimental error spans. Doc imp...David Aspinall
2009-09-10Disable debug message in IsarDavid Aspinall
2009-09-10Experimental changes to queue several commands at once and to allow pre-proce...David Aspinall
2009-09-10proof-retract-until-point: protect against finding no span at allDavid Aspinall
2009-09-10Clean compileDavid Aspinall
2009-09-09pg-last-output-displayform: strip trailing CR as well as initial one,David Aspinall
2009-09-09Delete the pghelp spans for now, after all.David Aspinall
2009-09-09proof-script-clear-queue-spans: scan less of bufferDavid Aspinall
2009-09-09proof-shell-error-or-interrupt-seen -> proof-shell-last-error-kind,David Aspinall
2009-09-07Fix compile warningsDavid Aspinall
2009-09-06pg-add-element: unbound var in debugDavid Aspinall
2009-09-06Tweak point movement in `proof-assert-until-point' andDavid Aspinall
2009-09-05Minor optDavid Aspinall
2009-09-05proof-set-queue-endpoints: no undo-make-selective-list (pg-protected-undo rep...David Aspinall
2009-09-05Clean whitespaceDavid Aspinall
2009-09-05Whitespaces and commentsDavid Aspinall
2009-09-04Add proof-script-evaluate-elisp-comment-regexp security hole.David Aspinall
2009-09-04proof-file-to-buffer -> find-buffer-visitingDavid Aspinall
2009-09-04Remove configuration of obsolete package function-menu (aka "fume")David Aspinall
2009-09-04Remove configuration of obsolete package function-menu (aka "fume")David Aspinall
2009-09-04Refactoring point movement commands (in progress). Remove proof-no-command.David Aspinall
2009-08-29Cleanup of interactive point moving functions (in progress)David Aspinall
2009-08-28Fix compile warningsDavid Aspinall