proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2010-08-17	Clean up handling of pending interrupts, remove experimental ↵	David Aspinall
	proof-shell-interrupts-after-commit.
2010-08-16	Fix compile errors, update tags	David Aspinall

2010-08-15	Preliminary and experimental support for automatically sending commands.	David Aspinall

2010-08-13	proof-activate-scripting: make sure can succeed when	David Aspinall
	proof-activate-scripting-hook does nothing (case: switching buffers in Coq when there was an error)
2010-08-11	Support custom syntactic fontification. Split out pa macros.	David Aspinall

2010-08-08	proof-assert-electric-terminator: give more user-friendly error message if ↵	David Aspinall
	unparseable
2010-08-08	Checkdoc cleanups	David Aspinall

2010-08-03	proof-assert-electric-terminator: fix logic for inserting at buffer end	David Aspinall

2010-08-03	Move key binding for proof assistant keymap (fixes compilation bug)	David Aspinall

2010-08-03	save-some-buffers: only offer to save proof script buffers	David Aspinall

2010-08-03	Add support for basic "movie" recording. See http://mws.cs.ru.nl/proviola.	David Aspinall

2010-07-08	Cleanups for save-excursion to avoid warnings in latest Emacs versions	David Aspinall

2009-12-03	Rework script span element hiding to avoid buffer-invisibility-spec. Add ↵	David Aspinall
	command elements.
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