proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2010-08-25	Renamed from plastic/plastic.el to obsolete/plastic/plastic.el	David Aspinall

2010-08-25	Renamed from plastic/README to obsolete/plastic/README	David Aspinall

2010-08-25	Renamed from plastic/plastic-syntax.el to obsolete/plastic/plastic-syntax.el	David Aspinall

2010-08-25	Renamed from plastic/test.lf to obsolete/plastic/test.lf	David Aspinall

2010-07-01	plastic-shell-adjust-line-width: save-excursion -> with-current-buffer to avoid	David Aspinall
	spurious warning in Emacs 23.2
2009-09-28	Functions find-and-forget and count-undos now return lists of commands	David Aspinall

2009-09-28	Update docs	David Aspinall

2009-09-15	Prevent compile warning	David Aspinall

2009-09-10	Clean compile and update config	David Aspinall

2009-09-09	p-s-classify-output -> p-s-handle-output, and simplify system-specific hook	David Aspinall

2009-09-08	Remove barely useful proof-shell-abort-goal-regexp (only served to sanitize ↵	David Aspinall
	LEGO messages)
2009-09-06	Configuration changes for shell mode revision.	David Aspinall

2009-09-06	Remove proof-shell-wakeup-char	David Aspinall

2009-09-05	Clean whitespace	David Aspinall

2009-09-04	replace-in-string -> replace-regexp-in-string	David Aspinall

2009-09-04	Remove proof-shell-prompt-pattern, no longer used.	David Aspinall

2009-08-14	Rename proof-shell-process-output -> proof-shell-classify-output	David Aspinall

2009-05-26	Fix header	David Aspinall

2008-07-24	Merge changes from Version4Branch.	David Aspinall

2008-02-17	Updated.	David Aspinall

2008-01-17	Updated keybinding syntax	David Aspinall

2008-01-15	Many compatibility updates, bug fixes, rearrangements for compilation.	David Aspinall

2007-12-13	Deleted file	David Aspinall

2007-08-14	Add support for sending back literal commands reusing PBP markup mechanisms.	David Aspinall

2006-04-26	Changed the type of proof-goal-command-p. It takes now a span, which	Pierre Courtieu
	allows using a span attribute to detect goal commands. I think I modified all modes accordingly.
2006-01-27	Fix from Paul	David Aspinall

2005-08-14	Fix plastic-shell-adjust-line-width for mutliple frame mode.	David Aspinall

2004-05-07	Fix for GNU Emacs	David Aspinall

2003-06-05	Make find-and-forget robust for proverproc regions	David Aspinall

2003-02-24	Fix some compile errors	David Aspinall

2002-08-29	Fix calls on proof-defshortcut	David Aspinall

2002-08-28	Fix interactive posn	David Aspinall

2002-08-07	Update from PC, sent 5.8.02	David Aspinall

2002-07-19	Variable name change proof-comment-{start,end}-regexp -> ↵	David Aspinall
	proof-script-comment-{start,end}-regexp.
2002-07-16	Refactor several variable names; clean up, doc subterm markup and output ↵	David Aspinall
	display.
2001-09-03	Add specific install instrs, rearrange.	David Aspinall

2000-06-09	Removed spurious requires.	David Aspinall

2000-06-08	adapted to new indentation setup;	Makarius Wenzel

2000-05-29	Fixed define-key calls. Set useful default for plastic prog name	David Aspinall

2000-05-26	fixed error in test.lf	Paul Callaghan
	fixed conflict in plastic.el
2000-05-02	Added proof-assistant-keymap and commands for defining insert keys.	David Aspinall

2000-04-07	pbp-mode -> goals-mode	David Aspinall

2000-04-07	Fixed up proof-shell-proof-completed mess nicely.	David Aspinall

2000-03-13	New/updated information files	David Aspinall

2000-01-06	Fixes for short output duplication problem: set ↵	David Aspinall
	proof-shell-eager-annotation-start-length.
1999-11-22	proof-shell-done-invisible -> proof-done-invisible again	David Aspinall

1999-11-17	Fix several bugs caused by interface changes.	David Aspinall

1999-11-15	Change name of proof-execute-minibufer-cmd.	David Aspinall

1999-11-15	Removed proof-try-command.	David Aspinall

1999-11-14	Many robustness improvements for error and interrupt handling:	David Aspinall
	- Introduce proof-shell-error-or-interrupt-seen flag set after an error or interrupt was seen (in fact, on every call to proof-release-lock). Examine it in proof-activate-scripting to see whether hooks succeeded in activating scripting. - Test in the shell filter for the lock being held yet nothing in the action list, and clear the lock if so. Gets rid of repetetive proof-shell-busy messages when the queue is empty (for errors during development, or nasty uses of C-g) - Add a timeout to proof-shell-wait (not used yet)