proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
1998-10-13	Disabled font-lock in process buffer	Thomas Kleymann

1998-10-12	Added compatibility hack for customize-menu-create.	David Aspinall

1998-10-12	Added sensible error message for attempting undo on empty locked region.	David Aspinall

1998-10-12	Made defface's work for dark background Emacsen (default for FSF on Linux).	David Aspinall

1998-10-12	Dox. Made proof-shell-exec-loop not complain about empty action list.	David Aspinall

1998-10-12	Splash screen tries gif if jpeg not available. Using hack by tms	David Aspinall

1998-10-12	Fixed typo.	David Aspinall

1998-10-12	Toolbar featurep. Separate Internals menu. Doc strings.	David Aspinall

1998-10-09	Customize group name: prover-config, not proof-config.	David Aspinall

1998-10-09	Minor bug fixes, code, doc improvements.	David Aspinall

1998-10-08	Changed binding for C-c RET	David Aspinall

1998-10-07	Added more documentation.	David Aspinall
	Made new proof-config customization group for variables supposed to be configured by prover specific settings (as opposed to user options, which are set by users). This adds type information and useful facility for testing new instances of PG. Similarly added proof-shell customization group. Removed (what I assume to be) defunct variables proof-post-shell-exit-hook, proof-shell-echo-input. Made deflocal do 'setq-default', not 'setq'. (I consider this a bugfix, but no calls to deflocal use other than nil value anyway, so this bug had no effect.) Added code for displaying splash screen. Attempted fix for proof-issue-new-command when process inactive. Improved functions proof-script-new-command-advance, proof-script-next-command-advance, called from proof-assert-next-command.
1998-10-05	da> BTW, the menus have disappeared!	Thomas Kleymann
	They are back courtesy of reintroducing an easy-menu-add call.
1998-10-02	Moved menu definition back into proof-config-done.	David Aspinall

1998-10-02	added LEGO support for proof-goal-command and proof-save-command	Thomas Kleymann

1998-10-01	Updated maintainer tags to remove lego email address.	David Aspinall

1998-10-01	Added docstrings and comments.	David Aspinall
	Removed last of "not authorized for this documentation" nonsense. Replaced constant string "COMMENT" by proof-no-command. Begun work on new functions: proof-{next,previous}-matching-command. Work on proof-issue-goal, proof-issue-save (rough edges left as FIXMEs).
1998-09-23	Changed customization group and removed nagging not-busy error message	David Aspinall

1998-09-22	Cleaned up and improved some code, added docstrings, FIXMEs.	David Aspinall
	Added proof-issue-goal and proof-goal-command. Rearranged to get ready for splitting into proof-script and proof-shell. Added proof-one-command-per-line user option.
1998-09-17	Fix in proof-shell-handle-output	David Aspinall

1998-09-17	fixed a bug in proof-shell-filter and proof-shell-handle-ouput	Thomas Kleymann

1998-09-16	Moved proof-info-dir into proof-site and defcustom'd it.	David Aspinall
	Set the Info directory list there rather than after proof.el has loaded. Add the proof-info-dir onto the end of Info-default-directory-list, not the start.
1998-09-16	fixed implementation fo proof-find-next-terminator;	Thomas Kleymann
	it can now be used even when there is no corresponding proof process
1998-09-16	Improved doc. Removed proof-mode-version-string.\nMade ↵	David Aspinall
	proof-prog-name-ask-p defcustom
1998-09-15	Reimplemented proof-shell-popup-eager-annotation	Thomas Kleymann
	These are no longer displayed in the GOALS buffer.
1998-09-14	Added docs and proof-restart-script-same-process (may need work)	David Aspinall

1998-09-10	-Added documentation	Thomas Kleymann
	-Simplified code for setting faces -Reimplimented `proof-shell-handle-error' -Improved `proof-shell-filter'; it no longer removes the prompt annotation -The Shell no longer automatically scrolls to the end (or so I hope)
1998-09-09	Made proof-assert-next-command move forward by default.	David Aspinall

1998-09-09	Added Id to headers.	David Aspinall

1998-09-08	Added FIXMEs.	David Aspinall
	Added documentation. proof-segment-up-to: Removed explicit ML-style comment syntax, added END-OF-COMMAND argument. proof-undo-last-successful-command: Added optional argument to not delete. (The difference between this and proof-retract-until-point is that it infers the last command). proof-assert-next-command: Experimental alternative to proof-assert-until-point to match undo-last-successful-command.
1998-09-08	removed dependency on tl-list	Thomas Kleymann

1998-09-03	Requires proof-site.	David Aspinall

1998-09-03	Renamed for new subdirectory structure	David Aspinall