proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Reorganization and cleanup of key-bindings.	David Aspinall	1999-11-15
\| \| \| \| \| \| \| \| \| \| \| \|	FSF fix for proof-cd. Fix for proof-goto-point. Made proof-done-advancing robust against unset proof-save-command-regexp. Improved several docstrings. Fixes for proof-frob-locked end, made disabled by default for novices. Fix for electric terminator indicator in non-PG buffers. Configuration variable proof-font-lock-zap-commas. Removed proof-try-command. Phew!
*	Added proof-splash-message.	David Aspinall	1999-11-15
\|
*	Fix for FSF Emacs. Added timeout arg to proof-shell-wait.	David Aspinall	1999-11-15
\|
*	Added in-testing message	David Aspinall	1999-11-15
\|
*	Removed font-lock settings. Set proof-font-lock-zap-commas=t	David Aspinall	1999-11-15
\|
*	Updated	David Aspinall	1999-11-15
\|
*	Tuned splash screen for FSF emacs. Added proof-font-lock-zap-commas	David Aspinall	1999-11-15
\|
*	Fixes for proof-goto-commmand-{end,start}. Former new function	David Aspinall	1999-11-14
\|
*	Many robustness improvements for error and interrupt handling:	David Aspinall	1999-11-14
\| \| \| \| \| \| \| \| \| \| \| \|	- 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)
*	docstring	David Aspinall	1999-11-14
\|
*	More highlighting	David Aspinall	1999-11-14
\|
*	Updated	David Aspinall	1999-11-14
\|
*	devel.clean : use find to clean all subdirs.	David Aspinall	1999-11-14
\|
*	Fix to docstring magic (allow spaces after symbol).	David Aspinall	1999-11-14
\|
*	proof-nested-goals-allowed -> proof-completed-proof-behaviour	David Aspinall	1999-11-14
\| \| \| \| \|	Patch for more flexible handling of closing goal...save regions after proof has been completed.
*	Add demoisa dir to makefiles.	David Aspinall	1999-11-14
\|
*	Beginnings of improved version of goal..no save regions.	David Aspinall	1999-11-13
\|
*	Updated	David Aspinall	1999-11-13
\|
*	clean: Remove autosaves and cvs server temporary files.	David Aspinall	1999-11-13
\|
*	comments	David Aspinall	1999-11-13
\|
*	Experiment with X-Symbol support for Coq.	David Aspinall	1999-11-13
\|
*	Call proof-goals-config-done properly.	David Aspinall	1999-11-13
\|
*	Use infix syntax	David Aspinall	1999-11-13
\|
*	Test case	David Aspinall	1999-11-13
\|
*	Added example instantiation demoisa	David Aspinall	1999-11-13
\|
*	Added new face for debug messages	David Aspinall	1999-11-13
\|
*	Updates and improvements	David Aspinall	1999-11-13
\|
*	Notes about font-lock management.	David Aspinall	1999-11-12
\|
*	Documentation improvements	David Aspinall	1999-11-12
\|
*	More theory file sections	David Aspinall	1999-11-12
\|
*	Fixes for Isabelle in case theory file is visited before script file.	David Aspinall	1999-11-12
\|
*	Document variables before functions in case of name clash.	David Aspinall	1999-11-12
\|
*	Added ACTION to proof-shell-insert so proof-shell-insert-hook can test class ↵	David Aspinall	1999-11-12
\| \| \| \|	of command. (For Plastic)
*	Set font-lock-keywords before calling proof-config-done.	David Aspinall	1999-11-12
\|
*	Made display table stuff interactive.	David Aspinall	1999-11-12
\|
*	Changed colour of proof-locked-face	David Aspinall	1999-11-12
\|
*	Fix for automode list	David Aspinall	1999-11-12
\|
*	Typo in x-symbol enable	David Aspinall	1999-11-12
\|
*	Typo in x-symbol enable	David Aspinall	1999-11-12
\|
*	Set version tag for new release.	David Aspinall	1999-11-12
\|
*	added nohup.out	David Aspinall	1999-11-12
\|
*	Updated	David Aspinall	1999-11-12
\|
*	Display qed message in goals buffer	David Aspinall	1999-11-12
\|
*	Fixes for response buffer display, x-symbol, output formatting.	David Aspinall	1999-11-12
\|
*	New testing files	David Aspinall	1999-11-12
\|
*	Updated	David Aspinall	1999-11-11
\|
*	Attempted x-symbol improvements	David Aspinall	1999-11-11
\|
*	Added option for sending qed output to goals buffer for Isabelle	David Aspinall	1999-11-11
\|
*	Improved documentation, more options added	David Aspinall	1999-11-11
\|
*	small changes to plastic mode	Paul Callaghan	1999-11-11
\|